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 ;

A1: now

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;

now

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;

then reconsider G9 = G9 as non empty Group-like associative strict HGrWOpStr of O by A1, GROUP_1:def 2, GROUP_1:def 3;
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 of O by Def5;

A2: now

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

A3: now

per cases ( o in O or not o in O ) ;

suppose A4: o in O ; :: thesis: G9 ^ o = G ^ o

then G9 ^ o = the action of G9 . o by Def6;
hence G9 ^ o = G ^ o by A4, Def6; :: thesis: verum

end;

suppose A5: not o in O ; :: thesis: G9 ^ o = G ^ o

then G9 ^ o = id the carrier of G9 by Def6;
hence G9 ^ o = G ^ o by A5, Def6; :: thesis: verum

end;

end;

end;

dom (G9 ^ o) = the carrier of G by FUNCT_2:def 1;
hence G9 ^ o = (G ^ o) | the carrier of G9 by A3, RELAT_1:69; :: thesis: verum

end;

dom the multF of G = [: the carrier of G9, the carrier of G9:] by FUNCT_2:def 1;
then the multF of G9 = the multF of G || the carrier of G9 by RELAT_1:68;
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