---

Step * of Lemma nat_op_mon_hom_1

∀[g:IMonoid]. ∀[a:|g|].  IsMonHom{<ℕ,+>,g}(λn.(n ⋅ a))
BY
{ ((Eval ``monoid_hom_p fun_thru_2op`` 0 
THENM Backchain ``mon_nat_op_zero mon_nat_op_add``) THENA Auto) }

---

Latex:

---

Latex:
\mforall{}[g:IMonoid].  \mforall{}[a:|g|].    IsMonHom\{<\mBbbN{},+>,g\}(\mlambda{}n.(n  \mcdot{}  a))


By

---

Latex:
((Eval  ``monoid\_hom\_p  fun\_thru\_2op``  0 
THENM  Backchain  ``mon\_nat\_op\_zero  mon\_nat\_op\_add``)  THENA  Auto)

---

Home Index