let O be set ; :: thesis: for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)

let H1, H2 be StableSubgroup of G; :: thesis: ( the carrier of H1 = the carrier of H2 implies HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #) )

reconsider H19 = H1, H29 = H2 as Subgroup of G by Def7;

A1: dom the action of H2 = O by FUNCT_2:def 1

.= dom the action of H1 by FUNCT_2:def 1 ;

assume A2: the carrier of H1 = the carrier of H2 ; :: thesis: HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)

hence HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #) by A1, A3, FUNCT_1:2; :: thesis: verum

for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)

let H1, H2 be StableSubgroup of G; :: thesis: ( the carrier of H1 = the carrier of H2 implies HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #) )

reconsider H19 = H1, H29 = H2 as Subgroup of G by Def7;

A1: dom the action of H2 = O by FUNCT_2:def 1

.= dom the action of H1 by FUNCT_2:def 1 ;

assume A2: the carrier of H1 = the carrier of H2 ; :: thesis: HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)

A3: now :: thesis: for x being object st x in dom the action of H2 holds

the action of H1 . x = the action of H2 . x

multMagma(# the carrier of H19, the multF of H19 #) = multMagma(# the carrier of H29, the multF of H29 #)
by A2, GROUP_2:59;the action of H1 . x = the action of H2 . x

let x be object ; :: thesis: ( x in dom the action of H2 implies the action of H1 . x = the action of H2 . x )

assume A4: x in dom the action of H2 ; :: thesis: the action of H1 . x = the action of H2 . x

then reconsider o = x as Element of O ;

A5: H1 ^ o = the action of H1 . o by A4, Def6;

H1 ^ o = (G ^ o) | the carrier of H2 by A2, Def7

.= H2 ^ o by Def7 ;

hence the action of H1 . x = the action of H2 . x by A4, A5, Def6; :: thesis: verum

end;assume A4: x in dom the action of H2 ; :: thesis: the action of H1 . x = the action of H2 . x

then reconsider o = x as Element of O ;

A5: H1 ^ o = the action of H1 . o by A4, Def6;

H1 ^ o = (G ^ o) | the carrier of H2 by A2, Def7

.= H2 ^ o by Def7 ;

hence the action of H1 . x = the action of H2 . x by A4, A5, Def6; :: thesis: verum

hence HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #) by A1, A3, FUNCT_1:2; :: thesis: verum