`∀[T,R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[f,g:T ⟶ R]. ∀[b:bag(T)].`
`  Σ(x∈b). f[x] add g[x] = (Σ(x∈b). f[x] add Σ(x∈b). g[x]) ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` comm: `Comm(T;op)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` infix_ap: `x f y` so_apply: `x[s]` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` monoid_p: `IsMonoid(T;op;id)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` prop: `ℙ` bag: `bag(T)` quotient: `x,y:A//B[x; y]` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` cand: `A c∧ B` monoid_p: `IsMonoid(T;op;id)` bag-summation: `Σ(x∈b). f[x]` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` top: `Top` infix_ap: `x f y` assoc: `Assoc(T;op)` true: `True` squash: `↓T` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` comm: `Comm(T;op)` ident: `Ident(T;op;id)`
Lemmas referenced :  monoid_p_wf comm_wf bag_wf list_wf quotient-member-eq permutation_wf permutation-equiv permutation_inversion equal_wf bag-summation_wf infix_ap_wf list-subtype-bag equal-wf-base list_induction all_wf list_accum_wf list_accum_nil_lemma list_accum_cons_lemma squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis productEquality extract_by_obid isectElimination cumulativity hypothesisEquality functionExtensionality applyEquality sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry functionEquality universeEquality pointwiseFunctionalityForEquality pertypeElimination lambdaFormation rename lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination hyp_replacement applyLambdaEquality independent_pairFormation voidElimination voidEquality natural_numberEquality imageElimination imageMemberEquality baseClosed

Latex:
\mforall{}[T,R:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[f,g:T  {}\mrightarrow{}  R].  \mforall{}[b:bag(T)].