let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st the carrier of H1 = the carrier of N1 holds
H1 ./. N1 is trivial
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st the carrier of H1 = the carrier of N1 holds
H1 ./. N1 is trivial
let H1 be StableSubgroup of G; :: thesis: for N1 being normal StableSubgroup of H1 st the carrier of H1 = the carrier of N1 holds
H1 ./. N1 is trivial
let N1 be normal StableSubgroup of H1; :: thesis: ( the carrier of H1 = the carrier of N1 implies H1 ./. N1 is trivial )
reconsider N1' = multMagma(# the carrier of N1,the multF of N1 #) as strict normal Subgroup of H1 by Lm7;
assume A1: the carrier of H1 = the carrier of N1 ; :: thesis: H1 ./. N1 is trivial

now

let x be set ; :: thesis: ( ( x in Left_Cosets N1' implies x = the carrier of H1 ) & ( x = the carrier of H1 implies x in Left_Cosets N1' ) )

hereby :: thesis: ( x = the carrier of H1 implies x in Left_Cosets N1' )

assume A2: x in Left_Cosets N1' ; :: thesis: x = the carrier of H1
then reconsider A = x as Subset of ;
consider a being Element of such that
A3: A = a * N1' by A2, GROUP_2:def 15;
A = a * ([#] the carrier of H1) by A1, A3;
hence x = the carrier of H1 by GROUP_2:21; :: thesis: verum

end;

the carrier of H1 = (1_ H1) * ([#] the carrier of H1) by GROUP_2:21;
then A4: the carrier of H1 = (1_ H1) * N1' by A1;
assume x = the carrier of H1 ; :: thesis: x in Left_Cosets N1'
hence x in Left_Cosets N1' by A4, GROUP_2:def 15; :: thesis: verum

end;

then A5: {the carrier of H1} = Left_Cosets N1' by TARSKI:def 1;
Cosets N1 = Cosets N1' by Def14;
hence H1 ./. N1 is trivial by A5, GROUP_6:def 2; :: thesis: verum