defpred S1[ set ] means g . $1 = 1_ H;
reconsider A = { a where a is Element of G : S1[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 GROUP_6:def 6
.= 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 Lm13
.= 1_ H by GROUP_1:8 ;
hence a " in A ; :: thesis: verum
end;
A4: now :: thesis: for o being Element of O
for a being Element of G st a in A holds
(G ^ o) . a in A
let o be Element of O; :: thesis: for a being Element of G st a in A holds
(G ^ o) . a in A
let a be Element of G; :: thesis: ( a in A implies (G ^ o) . a in A )
assume a in A ; :: thesis: (G ^ o) . a in A
then ex a1 being Element of G st
( a1 = a & g . a1 = 1_ H ) ;
then g . ((G ^ o) . a) = (H ^ o) . (1_ H) by Def18
.= 1_ H by GROUP_6:31 ;
hence (G ^ o) . a in A ; :: thesis: verum
end;
g . (1_ G) = 1_ H by Lm12;
then 1_ G in A ;
then consider B being strict StableSubgroup of G such that
A5: the carrier of B = A by A1, A3, A4, Lm14;
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 A5; :: thesis: verum