---

Step * 1 3 of Lemma oal_omcp_wf

.....wf..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. c : mcopower_sig{i:l}(s;g↓hgrp)
⊢ (∀j:|s|. IsMonHom{g↓hgrp,c.mon}(c.inj j))
  ∧ (∀h:AbMon. ∀f:|s| ⟶ MonHom(g↓hgrp,h).
       (c.umap h f) = !v:|c.mon| ⟶ |h|
                        (IsMonHom{c.mon,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|(g↓hgrp)| ⟶ |h|))))) ∈ 𝕌'
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  c  :  mcopower\_sig\{i:l\}(s;g\mdownarrow{}hgrp)
\mvdash{}  (\mforall{}j:|s|.  IsMonHom\{g\mdownarrow{}hgrp,c.mon\}(c.inj  j))
    \mwedge{}  (\mforall{}h:AbMon.  \mforall{}f:|s|  {}\mrightarrow{}  MonHom(g\mdownarrow{}hgrp,h).
              (c.umap  h  f)  =  !v:|c.mon|  {}\mrightarrow{}  |h|
                                                (IsMonHom\{c.mon,h\}(v)  \mwedge{}  (\mforall{}j:|s|.  ((f  j)  =  (v  o  (c.inj  j))))))  \mmember{}  \mBbbU{}'


By

---

Latex:
Auto

---

Home Index