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 #)
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
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;
multMagma(# the carrier of H19, the multF of H19 #) = multMagma(# the carrier of H29, the multF of H29 #) by A2, GROUP_2:59;
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