defpred S₁[ set ] means g . $1 = 1_ H;
reconsider A = { a where a is Element of G : S₁[a] } as Subset of G from DOMAIN_1:sch 7();

A1: now :: thesis: for a, b being Element of G st a in A & b in A holds
a * b in A

let a, b be Element of G; :: thesis: ( a in A & b in A implies a * b in A )
assume ( a in A & b in A ) ; :: thesis: a * b in A
then A2: ( ex a1 being Element of G st
( a1 = a & g . a1 = 1_ H ) & ex b1 being Element of G st
( b1 = b & g . b1 = 1_ H ) ) ;
g . (a * b) = (g . a) * (g . b) by Def6
.= 1_ H by A2, GROUP_1:def 4 ;
hence a * b in A ; :: thesis: verum

end;

A3: now :: thesis: for a being Element of G st a in A holds
a " in A

let a be Element of G; :: thesis: ( a in A implies a " in A )
assume a in A ; :: thesis: a " in A
then ex a1 being Element of G st
( a1 = a & g . a1 = 1_ H ) ;
then g . (a ") = (1_ H) " by Th32
.= 1_ H by GROUP_1:8 ;
hence a " in A ; :: thesis: verum

end;

g . (1_ G) = 1_ H by Th31;
then 1_ G in A ;
then consider B being strict Subgroup of G such that
A4: the carrier of B = A by A1, A3, GROUP_2:52;
reconsider B = B as strict Subgroup of G ;
take B ; :: thesis: the carrier of B = { a where a is Element of G : g . a = 1_ H }
thus the carrier of B = { a where a is Element of G : g . a = 1_ H } by A4; :: thesis: verum