---

Step * of Lemma gcopower_grp_wf

∀s:PosetSig. ∀g:GrpSig. ∀g1:gcopower_sig{i:l}(s;g).  (g1.grp ∈ GrpSig)
BY
{ ModulePiTac 3 ``gcopower_grp gcopower_inj gcopower_umap`` }

---

Latex:

---

Latex:
\mforall{}s:PosetSig.  \mforall{}g:GrpSig.  \mforall{}g1:gcopower\_sig\{i:l\}(s;g).    (g1.grp  \mmember{}  GrpSig)


By

---

Latex:
ModulePiTac  3  ``gcopower\_grp  gcopower\_inj  gcopower\_umap``

---

Home Index