the carrier of G c= the carrier of G ;
then reconsider X = the carrier of G as Subset of G ;
set S = g .: X;

A1: now :: thesis: for c, d being Element of H st c in g .: X & d in g .: X holds
c * d in g .: X

let c, d be Element of H; :: thesis: ( c in g .: X & d in g .: X implies c * d in g .: X )
assume that
A2: c in g .: X and
A3: d in g .: X ; :: thesis: c * d in g .: X
consider b being Element of G such that
b in X and
A4: d = g . b by A3, FUNCT_2:65;
consider a being Element of G such that
a in X and
A5: c = g . a by A2, FUNCT_2:65;
c * d = g . (a * b) by A5, A4, Def6;
hence c * d in g .: X by FUNCT_2:35; :: thesis: verum

end;

A6: now :: thesis: for c being Element of H st c in g .: X holds
c " in g .: X

let c be Element of H; :: thesis: ( c in g .: X implies c " in g .: X )
assume c in g .: X ; :: thesis: c " in g .: X
then consider a being Element of G such that
a in X and
A7: c = g . a by FUNCT_2:65;
g . (a ") = c " by A7, Th32;
hence c " in g .: X by FUNCT_2:35; :: thesis: verum

end;

dom g = the carrier of G by FUNCT_2:def 1;
then consider D being strict Subgroup of H such that
A8: the carrier of D = g .: X by A1, A6, GROUP_2:52;
take D ; :: thesis: the carrier of D = g .: the carrier of G
thus the carrier of D = g .: the carrier of G by A8; :: thesis: verum