let O be set ; :: thesis: for G being GroupWithOperators of O holds HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G

let G be GroupWithOperators of O; :: thesis: HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G

reconsider G9 = HGrWOpStr(# the carrier of G, the multF of G, the action of G #) as non empty multMagma ;

for G being Group

for a being Action of O, the carrier of G st a = the action of G9 & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of G9, the multF of G9 #) holds

a is distributive by Def5;

then reconsider G9 = G9 as non empty Group-like associative distributive HGrWOpStr over O by Def5;

then G9 is Subgroup of G by GROUP_2:def 5;

hence HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G by A2, Def7; :: thesis: verum

let G be GroupWithOperators of O; :: thesis: HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G

reconsider G9 = HGrWOpStr(# the carrier of G, the multF of G, the action of G #) as non empty multMagma ;

A1: now :: thesis: ex e9 being Element of G9 st

for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

set e = 1_ G;

reconsider e9 = 1_ G as Element of G9 ;

take e9 = e9; :: thesis: for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

let h9 be Element of G9; :: thesis: ( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

reconsider h = h9 as Element of G ;

set g = h " ;

reconsider g9 = h " as Element of G9 ;

h9 * e9 = h * (1_ G)

.= h by GROUP_1:def 4 ;

hence h9 * e9 = h9 ; :: thesis: ( e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

e9 * h9 = (1_ G) * h

.= h by GROUP_1:def 4 ;

hence e9 * h9 = h9 ; :: thesis: ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 )

take g9 = g9; :: thesis: ( h9 * g9 = e9 & g9 * h9 = e9 )

h9 * g9 = h * (h ")

.= 1_ G by GROUP_1:def 5 ;

hence h9 * g9 = e9 ; :: thesis: g9 * h9 = e9

g9 * h9 = (h ") * h

.= 1_ G by GROUP_1:def 5 ;

hence g9 * h9 = e9 ; :: thesis: verum

end;reconsider e9 = 1_ G as Element of G9 ;

take e9 = e9; :: thesis: for h9 being Element of G9 holds

( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

let h9 be Element of G9; :: thesis: ( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

reconsider h = h9 as Element of G ;

set g = h " ;

reconsider g9 = h " as Element of G9 ;

h9 * e9 = h * (1_ G)

.= h by GROUP_1:def 4 ;

hence h9 * e9 = h9 ; :: thesis: ( e9 * h9 = h9 & ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 ) )

e9 * h9 = (1_ G) * h

.= h by GROUP_1:def 4 ;

hence e9 * h9 = h9 ; :: thesis: ex g9 being Element of G9 st

( h9 * g9 = e9 & g9 * h9 = e9 )

take g9 = g9; :: thesis: ( h9 * g9 = e9 & g9 * h9 = e9 )

h9 * g9 = h * (h ")

.= 1_ G by GROUP_1:def 5 ;

hence h9 * g9 = e9 ; :: thesis: g9 * h9 = e9

g9 * h9 = (h ") * h

.= 1_ G by GROUP_1:def 5 ;

hence g9 * h9 = e9 ; :: thesis: verum

now :: thesis: for x9, y9, z9 being Element of G9 holds (x9 * y9) * z9 = x9 * (y9 * z9)

then reconsider G9 = G9 as non empty Group-like associative strict HGrWOpStr over O by A1, GROUP_1:def 2, GROUP_1:def 3;let x9, y9, z9 be Element of G9; :: thesis: (x9 * y9) * z9 = x9 * (y9 * z9)

reconsider x = x9, y = y9, z = z9 as Element of G ;

(x9 * y9) * z9 = (x * y) * z

.= x * (y * z) by GROUP_1:def 3 ;

hence (x9 * y9) * z9 = x9 * (y9 * z9) ; :: thesis: verum

end;reconsider x = x9, y = y9, z = z9 as Element of G ;

(x9 * y9) * z9 = (x * y) * z

.= x * (y * z) by GROUP_1:def 3 ;

hence (x9 * y9) * z9 = x9 * (y9 * z9) ; :: thesis: verum

for G being Group

for a being Action of O, the carrier of G st a = the action of G9 & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of G9, the multF of G9 #) holds

a is distributive by Def5;

then reconsider G9 = G9 as non empty Group-like associative distributive HGrWOpStr over O by Def5;

A2: now :: thesis: for o being Element of O holds G9 ^ o = (G ^ o) | the carrier of G9

the multF of G9 = the multF of G || the carrier of G9
;let o be Element of O; :: thesis: G9 ^ o = (G ^ o) | the carrier of G9

end;A3: now :: thesis: G9 ^ o = G ^ oend;

thus
G9 ^ o = (G ^ o) | the carrier of G9
by A3; :: thesis: verumthen G9 is Subgroup of G by GROUP_2:def 5;

hence HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G by A2, Def7; :: thesis: verum