### Nuprl Lemma : bag-summation_wf

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

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` comm: `Comm(T;op)` assoc: `Assoc(T;op)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` and: `P ∧ Q` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bag-summation: `Σ(x∈b). f[x]` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` prop: `ℙ` true: `True` infix_ap: `x f y` guard: `{T}` assoc: `Assoc(T;op)` squash: `↓T` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` comm: `Comm(T;op)`
Lemmas referenced :  bag-accum_wf assoc_wf comm_wf bag_wf equal_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin extract_by_obid isectElimination cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality because_Cache independent_isectElimination lambdaFormation hypothesis axiomEquality equalityTransitivity equalitySymmetry productEquality isect_memberEquality functionEquality universeEquality natural_numberEquality imageElimination imageMemberEquality baseClosed independent_functionElimination

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