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 G' = HGrWOpStr(# the carrier of G,the multF of G,the action of G #) as non empty multMagma ;

A1: now

set e = 1_ G;
reconsider e' = 1_ G as Element of ;
take e' = e'; :: thesis: for h' being Element of holds
( h' * e' = h' & e' * h' = h' & ex g' being Element of st
( h' * g' = e' & g' * h' = e' ) )
let h' be Element of ; :: thesis: ( h' * e' = h' & e' * h' = h' & ex g' being Element of st
( h' * g' = e' & g' * h' = e' ) )
reconsider h = h' as Element of ;
set g = h " ;
reconsider g' = h " as Element of ;
h' * e' = h * (1_ G)
.= h by GROUP_1:def 5 ;
hence h' * e' = h' ; :: thesis: ( e' * h' = h' & ex g' being Element of st
( h' * g' = e' & g' * h' = e' ) )
e' * h' = (1_ G) * h
.= h by GROUP_1:def 5 ;
hence e' * h' = h' ; :: thesis: ex g' being Element of st
( h' * g' = e' & g' * h' = e' )
take g' = g'; :: thesis: ( h' * g' = e' & g' * h' = e' )
h' * g' = h * (h " )
.= 1_ G by GROUP_1:def 6 ;
hence h' * g' = e' ; :: thesis: g' * h' = e'
g' * h' = (h " ) * h
.= 1_ G by GROUP_1:def 6 ;
hence g' * h' = e' ; :: thesis: verum

end;

now

let x', y', z' be Element of ; :: thesis: (x' * y') * z' = x' * (y' * z')
reconsider x = x', y = y', z = z' as Element of ;
(x' * y') * z' = (x * y) * z
.= x * (y * z) by GROUP_1:def 4 ;
hence (x' * y') * z' = x' * (y' * z') ; :: thesis: verum

end;

then reconsider G' = G' as non empty Group-like associative strict HGrWOpStr of O by A1, GROUP_1:def 3, GROUP_1:def 4;
for G being Group
for a being Action of O,the carrier of G st a = the action of G' & multMagma(# the carrier of G,the multF of G #) = multMagma(# the carrier of G',the multF of G' #) holds
a is distributive by Def5;
then reconsider G' = G' as non empty Group-like associative distributive HGrWOpStr of O by Def5;

A2: now

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

A3: now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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