---

Step * 1 of Lemma bag-summation-hom


1. r : Rng
2. s : Rng
3. IsMonoid(|s|;+s;0)
4. IsMonoid(|r|;+r;0)
5. f : |r| ⟶ |s|
6. rng_hom_p(r;s;f)
7. A : Type
8. g : A ⟶ |r|
⊢ 0 = f[0] ∈ |s|
BY
{ (FLemma `rng_hom_zero` [-3] THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  s  :  Rng
3.  IsMonoid(|s|;+s;0)
4.  IsMonoid(|r|;+r;0)
5.  f  :  |r|  {}\mrightarrow{}  |s|
6.  rng\_hom\_p(r;s;f)
7.  A  :  Type
8.  g  :  A  {}\mrightarrow{}  |r|
\mvdash{}  0  =  f[0]


By

---

Latex:
(FLemma  `rng\_hom\_zero`  [-3]  THEN  Auto)

---

Home Index