---

Step * of Lemma oal_inj_mon_hom

∀a:LOSet. ∀b:AbDMon. ∀k:|a|.  IsMonHom{b,oal_mon(a;b)}(λv.inj(k,v))
BY
{ ((Force `5` (Eval ``monoid_hom_p fun_thru_2op`` 0) 
THEN GenRepD) THENA Auto) }

1
1. a : LOSet
2. b : AbDMon
3. k : |a|
4. a1 : |b|
5. a2 : |b|
⊢ inj(k,a1 * a2) = (inj(k,a1) ++ inj(k,a2)) ∈ |oal(a;b)|

2
1. a : LOSet
2. b : AbDMon
3. k : |a|
⊢ inj(k,e) = 00 ∈ |oal(a;b)|

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDMon.  \mforall{}k:|a|.    IsMonHom\{b,oal\_mon(a;b)\}(\mlambda{}v.inj(k,v))


By

---

Latex:
((Force  `5`  (Eval  ``monoid\_hom\_p  fun\_thru\_2op``  0) 
THEN  GenRepD)  THENA  Auto)

---

Home Index