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

Cosets N1 = Cosets N19 by Def14;

hence H1 ./. N1 is trivial by A5; :: thesis: verum

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 ) )

then A5:
{ the carrier of H1} = Left_Cosets N19
by TARSKI:def 1;( ( 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 ) )

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;hereby :: thesis: ( x = the carrier of H1 implies x in Left_Cosets N19 )

the carrier of H1 = (1_ H1) * ([#] the carrier of H1)
by GROUP_2:17;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;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

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

Cosets N1 = Cosets N19 by Def14;

hence H1 ./. N1 is trivial by A5; :: thesis: verum