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 H1 ./. N1 is trivial holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

let H1 be StableSubgroup of G; :: thesis: for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

let N1 be normal StableSubgroup of H1; :: thesis: ( H1 ./. N1 is trivial implies HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #) )

reconsider N9 = N1 as StableSubgroup of G by Th11;

set H = H1;

reconsider N = multMagma(# the carrier of N1, the multF of N1 #) as normal Subgroup of H1 by Lm6;

assume A1: H1 ./. N1 is trivial ; :: thesis: HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

Cosets N1 = Cosets N by Def14;

then consider e being object such that

A2: the carrier of (H1 ./. N) = {e} by A1;

A3: the carrier of H1 = union {e} by A2, GROUP_2:137;

then the carrier of N9 = the carrier of H1 by A4, XBOOLE_0:def 10;

hence HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #) by Th75; :: thesis: verum

for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G

for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

let H1 be StableSubgroup of G; :: thesis: for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds

HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

let N1 be normal StableSubgroup of H1; :: thesis: ( H1 ./. N1 is trivial implies HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #) )

reconsider N9 = N1 as StableSubgroup of G by Th11;

set H = H1;

reconsider N = multMagma(# the carrier of N1, the multF of N1 #) as normal Subgroup of H1 by Lm6;

assume A1: H1 ./. N1 is trivial ; :: thesis: HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

Cosets N1 = Cosets N by Def14;

then consider e being object such that

A2: the carrier of (H1 ./. N) = {e} by A1;

A3: the carrier of H1 = union {e} by A2, GROUP_2:137;

A4: now :: thesis: the carrier of H1 c= the carrier of N

the carrier of N c= the carrier of H1
by GROUP_2:def 5;assume
not the carrier of H1 c= the carrier of N
; :: thesis: contradiction

then the carrier of H1 \ the carrier of N <> {} by XBOOLE_1:37;

then consider x being object such that

A5: x in the carrier of H1 \ the carrier of N by XBOOLE_0:def 1;

reconsider x = x as Element of H1 by A5;

hence contradiction by A2, A6, TARSKI:def 1; :: thesis: verum

end;then the carrier of H1 \ the carrier of N <> {} by XBOOLE_1:37;

then consider x being object such that

A5: x in the carrier of H1 \ the carrier of N by XBOOLE_0:def 1;

reconsider x = x as Element of H1 by A5;

A6: now :: thesis: not x * N = e

x * N in Cosets N
by GROUP_6:14;assume
x * N = e
; :: thesis: contradiction

then x * N = the carrier of H1 by A3, ZFMISC_1:25;

then consider x9 being Element of H1 such that

A7: 1_ H1 = x * x9 and

A8: x9 in N by GROUP_2:103;

x9 = x " by A7, GROUP_1:12;

then (x ") " in N by A8, GROUP_2:51;

then x in carr N by STRUCT_0:def 5;

hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;then x * N = the carrier of H1 by A3, ZFMISC_1:25;

then consider x9 being Element of H1 such that

A7: 1_ H1 = x * x9 and

A8: x9 in N by GROUP_2:103;

x9 = x " by A7, GROUP_1:12;

then (x ") " in N by A8, GROUP_2:51;

then x in carr N by STRUCT_0:def 5;

hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

hence contradiction by A2, A6, TARSKI:def 1; :: thesis: verum

then the carrier of N9 = the carrier of H1 by A4, XBOOLE_0:def 10;

hence HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #) by Th75; :: thesis: verum