let G be Group; :: thesis: for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H
let H be Subgroup of G; :: thesis: ((Omega). G) /\ H = (Omega). H
reconsider G9 = (Omega). G as strict Group ;
( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def 5;
then reconsider H9 = (Omega). H as strict Subgroup of G9 by GROUP_2:def 5;
( the carrier of H c= the carrier of G & the multF of H = the multF of G || the carrier of H ) by GROUP_2:def 5;
then A1: H is Subgroup of (Omega). G by GROUP_2:def 5;
multMagma(# the carrier of (((Omega). G) /\ H), the multF of (((Omega). G) /\ H) #) = multMagma(# the carrier of (H /\ ((Omega). G)), the multF of (H /\ ((Omega). G)) #)
.= multMagma(# the carrier of (H /\ ((Omega). G)), the multF of (H /\ ((Omega). G)) #)
.= multMagma(# the carrier of H, the multF of H #) by A1, GROUP_2:89
.= multMagma(# the carrier of (H9 /\ ((Omega). G9)), the multF of (H9 /\ ((Omega). G9)) #) by GROUP_2:89
.= multMagma(# the carrier of (H9 /\ ((Omega). G9)), the multF of (H9 /\ ((Omega). G9)) #)
.= multMagma(# the carrier of (((Omega). G9) /\ H9), the multF of (((Omega). G9) /\ H9) #) ;
hence ((Omega). G) /\ H = (Omega). H by GROUP_2:86; :: thesis: verum