let O be set ; :: thesis: for G being GroupWithOperators of O
for H being StableSubgroup of G holds multMagma(# the carrier of H,the multF of H #) is strict Subgroup of G
let G be GroupWithOperators of O; :: thesis: for H being StableSubgroup of G holds multMagma(# the carrier of H,the multF of H #) is strict Subgroup of G
let H be StableSubgroup of G; :: thesis: multMagma(# the carrier of H,the multF of H #) is strict Subgroup of G
reconsider H' = multMagma(# the carrier of H,the multF of H #) as non empty multMagma ;

now

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

end;

then reconsider H' = H' as non empty Group-like multMagma by GROUP_1:def 3;
H is Subgroup of G by Def7;
then ( the carrier of H' c= the carrier of G & the multF of H' = the multF of G || the carrier of H' ) by GROUP_2:def 5;
hence multMagma(# the carrier of H,the multF of H #) is strict Subgroup of G by GROUP_2:def 5; :: thesis: verum