---

Step * 1 2 1 1 of Lemma oal_omcp_wf


1. s : LOSet@i'
2. g : OGrp@i'
3. j : |s|@i
⊢ IsMonHom{g↓hgrp,oal_hgp(s;g)}(λv.inj(j,v))
BY
{ (((Unfold `monoid_hom_p` 0 
   THEN RWH oal_hgp_to_monC 0 
   THEN Fold `monoid_hom_p` 0 
   THEN BLemma `oal_inj_mon_hom`) THEN Auto)
   THEN BLemma `omon_inc`
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  j  :  |s|@i
\mvdash{}  IsMonHom\{g\mdownarrow{}hgrp,oal\_hgp(s;g)\}(\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  BLemma  `oal\_inj\_mon\_hom`)  THEN  Auto)
  THEN  BLemma  `omon\_inc`
  THEN  Auto)\mcdot{}

---

Home Index