Step
*
of Lemma
bag-summation-empty
∀[add,zero,f:Top]. (Σ(x∈{}). f[x] ~ zero)
BY
{ (RepUR ``bag-summation bag-accum empty-bag`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[add,zero,f:Top]. (\mSigma{}(x\mmember{}\{\}). f[x] \msim{} zero)
By
Latex:
(RepUR ``bag-summation bag-accum empty-bag`` 0 THEN Auto)
Home
Index