defpred S_{1}[ set ] means g . $1 = 1_ H;

reconsider A = { a where a is Element of G : S_{1}[a] } as Subset of G from DOMAIN_1:sch 7();

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

reconsider A = { a where a is Element of G : S

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

a * b in A

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;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

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

a " in A

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;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

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

g . (1_ G) = 1_ H
by Lm12;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 ^ 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

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