---

Step * 1 1 1 1 of Lemma bag-summation-add


1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. zero : R
5. f : T ⟶ R
6. g : T ⟶ R
7. IsMonoid(R;add;zero)
8. Comm(R;add)
⊢ ∀x,y,z:R.  ((z = add[x;y] ∈ R) ⇒ (z = add[x;y] ∈ R))
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  Type
3.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
4.  zero  :  R
5.  f  :  T  {}\mrightarrow{}  R
6.  g  :  T  {}\mrightarrow{}  R
7.  IsMonoid(R;add;zero)
8.  Comm(R;add)
\mvdash{}  \mforall{}x,y,z:R.    ((z  =  add[x;y])  {}\mRightarrow{}  (z  =  add[x;y]))


By

---

Latex:
Auto

---

Home Index