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 H9 = multMagma(# the carrier of H, the multF of H #) as non empty multMagma ;
now :: thesis: ex e9 being Element of H9 st
for h9 being Element of H9 holds
( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H9 st
( h9 * g9 = e9 & g9 * h9 = e9 ) )
set e = 1_ H;
reconsider e9 = 1_ H as Element of H9 ;
take e9 = e9; :: thesis: for h9 being Element of H9 holds
( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H9 st
( h9 * g9 = e9 & g9 * h9 = e9 ) )
let h9 be Element of H9; :: thesis: ( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of H9 st
( h9 * g9 = e9 & g9 * h9 = e9 ) )
reconsider h = h9 as Element of H ;
set g = h " ;
reconsider g9 = h " as Element of H9 ;
h9 * e9 = h * (1_ H)
.= h by GROUP_1:def 4 ;
hence h9 * e9 = h9 ; :: thesis: ( e9 * h9 = h9 & ex g9 being Element of H9 st
( h9 * g9 = e9 & g9 * h9 = e9 ) )
e9 * h9 = (1_ H) * h
.= h by GROUP_1:def 4 ;
hence e9 * h9 = h9 ; :: thesis: ex g9 being Element of H9 st
( h9 * g9 = e9 & g9 * h9 = e9 )
take g9 = g9; :: thesis: ( h9 * g9 = e9 & g9 * h9 = e9 )
h9 * g9 = h * (h ")
.= 1_ H by GROUP_1:def 5 ;
hence h9 * g9 = e9 ; :: thesis: g9 * h9 = e9
g9 * h9 = (h ") * h
.= 1_ H by GROUP_1:def 5 ;
hence g9 * h9 = e9 ; :: thesis: verum
end;
then reconsider H9 = H9 as non empty Group-like multMagma by GROUP_1:def 2;
H is Subgroup of G by Def7;
then ( the carrier of H9 c= the carrier of G & the multF of H9 = the multF of G || the carrier of H9 ) 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