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 N19 = multMagma(# the carrier of N1, the multF of N1 #) as strict normal Subgroup of H1 by Lm6;
assume A1: the carrier of H1 = the carrier of N1 ; :: thesis: H1 ./. N1 is trivial
now :: thesis: for x being object holds
( ( x in Left_Cosets N19 implies x = the carrier of H1 ) & ( x = the carrier of H1 implies x in Left_Cosets N19 ) )
let x be object ; :: thesis: ( ( x in Left_Cosets N19 implies x = the carrier of H1 ) & ( x = the carrier of H1 implies x in Left_Cosets N19 ) )
hereby :: thesis: ( x = the carrier of H1 implies x in Left_Cosets N19 )
assume A2: x in Left_Cosets N19 ; :: thesis: x = the carrier of H1
then reconsider A = x as Subset of H1 ;
consider a being Element of H1 such that
A3: A = a * N19 by A2, GROUP_2:def 15;
A = a * ([#] the carrier of H1) by A1, A3;
hence x = the carrier of H1 by GROUP_2:17; :: thesis: verum
end;
the carrier of H1 = (1_ H1) * ([#] the carrier of H1) by GROUP_2:17;
then A4: the carrier of H1 = (1_ H1) * N19 by A1;
assume x = the carrier of H1 ; :: thesis: x in Left_Cosets N19
hence x in Left_Cosets N19 by A4, GROUP_2:def 15; :: thesis: verum
end;
then A5: { the carrier of H1} = Left_Cosets N19 by TARSKI:def 1;
Cosets N1 = Cosets N19 by Def14;
hence H1 ./. N1 is trivial by A5; :: thesis: verum