let O be set ; :: thesis: for G being GroupWithOperators of O
for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
H1 = H2
let G be GroupWithOperators of O; :: thesis: for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
H1 = H2
let H1, H2 be strict StableSubgroup of G; :: thesis: ( the carrier of H1 = the carrier of H2 implies H1 = H2 )
assume A1: the carrier of H1 = the carrier of H2 ; :: thesis: H1 = H2
reconsider H1' = H1, H2' = H2 as Subgroup of G by Def7;
A2: multMagma(# the carrier of H1',the multF of H1' #) = multMagma(# the carrier of H2',the multF of H2' #) by A1, GROUP_2:68;
A3: dom the action of H2 = O by FUNCT_2:def 1
.= dom the action of H1 by FUNCT_2:def 1 ;

now

let x be set ; :: 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 & H2 ^ o = the action of H2 . o ) by A4, Def6;
H1 ^ o = (G ^ o) | the carrier of H2 by A1, Def7
.= H2 ^ o by Def7 ;
hence the action of H1 . x = the action of H2 . x by A5; :: thesis: verum

end;

hence H1 = H2 by A2, A3, FUNCT_1:9; :: thesis: verum