defpred S₁[ set ] means g . G = 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;

now :: thesis: for a being Element of G holds B |^ a is Subgroup of B

let a be Element of G; :: thesis: B |^ a is Subgroup of B

now :: thesis: for b being Element of G st b in B |^ a holds
b in B

let b be Element of G; :: thesis: ( b in B |^ a implies b in B )
assume b in B |^ a ; :: thesis: b in B
then consider c being Element of G such that
A5: b = c |^ a and
A6: c in B by GROUP_3:58;
c in A by A4, A6;
then ex a1 being Element of G st
( c = a1 & g . a1 = 1_ H ) ;
then g . b = (1_ H) |^ (g . a) by A5, Th33
.= 1_ H by GROUP_3:17 ;
then b in A ;
hence b in B by A4; :: thesis: verum

end;

hence B |^ a is Subgroup of B by GROUP_2:58; :: thesis: verum

end;

then B is normal Subgroup of G by GROUP_3:122;
hence Ker g is normal by A4, Def9; :: thesis: verum