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 ;

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

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 ) )

then reconsider H9 = H9 as non empty Group-like multMagma by GROUP_1:def 2;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;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

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