let G be Group; :: thesis: for A being Subgroup of G holds A is Subgroup of (Omega). G
let A be Subgroup of G; :: thesis: A is Subgroup of (Omega). G
dom the multF of G c= [: the carrier of G, the carrier of G:] ;
then the multF of G = the multF of ((Omega). G) || the carrier of ((Omega). G) by RELAT_1:68;
then G is Subgroup of (Omega). G by GROUP_2:def 5;
hence A is Subgroup of (Omega). G by GROUP_2:56; :: thesis: verum