---

Step * of Lemma oal_omcp_wf

∀s:LOSet. ∀g:OGrp.  (oal_omcp{s,g} ∈ MCopower(s;g↓hgrp))
BY
{ % The proof here needs cleaning up. It is quickly hacked 
  together from an older proof when the oal_umap definition had not 
  been made %  
((Unfold `oal_omcp` 0 THENM RepD) THENA Auto) }

1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ <oal_hgp(s;g), λk,v. inj(k,v), λh,f. umap(h,f)> ∈ MCopower(s;g↓hgrp)

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.    (oal\_omcp\{s,g\}  \mmember{}  MCopower(s;g\mdownarrow{}hgrp))


By

---

Latex:
\%  The  proof  here  needs  cleaning  up.  It  is  quickly  hacked 
    together  from  an  older  proof  when  the  oal\_umap  definition  had  not 
    been  made  \%   
((Unfold  `oal\_omcp`  0  THENM  RepD)  THENA  Auto)

---

Home Index