---

Step * 1 2 2 1 of Lemma oal_omcp_wf


1. s : LOSet@i'
2. g : OGrp@i'
3. ∀j:|s|. IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. uma\000Cp(h,f)>.inj j)
4. h : AbMon@i'
5. f : |s| ⟶ MonHom(g↓hgrp,h)@i
⊢ umap(h,f) = !v:|oal(s;g↓hgrp)| ⟶ |h|
                (IsMonHom{oal_hgp(s;g),h}(v) ∧ (∀j:|s|. ((f j) = (v o (λv.inj(j,v))) ∈ (|g|+ ⟶ |h|))))
BY
{ Unfold `monoid_hom_p` 0 
THEN RWH oal_hgp_to_monC 0 
THEN Fold `monoid_hom_p` 0 
THEN RWH hgrp_of_ocgrpC 0 }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ∀j:|s|. IsMonHom{g↓hgrp,<oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)>.mon}(<oal_hgp(s;g), λk,v. inj(k,v), λh,f. uma\000Cp(h,f)>.inj j)
4. h : AbMon@i'
5. f : |s| ⟶ MonHom(g↓hgrp,h)@i
⊢ umap(h,f) = !v:|oal(s;g↓hgrp)| ⟶ |h|
                (IsMonHom{oal_mon(s;g↓hgrp),h}(v) ∧ (∀j:|s|. ((f j) = (v o (λv.inj(j,v))) ∈ (|(g↓hgrp)| ⟶ |h|))))

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  \mforall{}j:|s|.  IsMonHom\{g\mdownarrow{}hgrp,<oal\_hgp(s;g),  \mlambda{}k,v.  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.mon\}(<oal\_hgp(s;g),  \mlambda{}k,v.\000C  inj(k,v),  \mlambda{}h,f.  umap(h,f)>.inj  j)
4.  h  :  AbMon@i'
5.  f  :  |s|  {}\mrightarrow{}  MonHom(g\mdownarrow{}hgrp,h)@i
\mvdash{}  umap(h,f)  =  !v:|oal(s;g\mdownarrow{}hgrp)|  {}\mrightarrow{}  |h|
                                (IsMonHom\{oal\_hgp(s;g),h\}(v)  \mwedge{}  (\mforall{}j:|s|.  ((f  j)  =  (v  o  (\mlambda{}v.inj(j,v))))))


By

---

Latex:
Unfold  `monoid\_hom\_p`  0 
THEN  RWH  oal\_hgp\_to\_monC  0 
THEN  Fold  `monoid\_hom\_p`  0 
THEN  RWH  hgrp\_of\_ocgrpC  0

---

Home Index