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;
A4: now :: thesis: the carrier of H1 c= the carrier of N
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;
A6: now :: thesis: not x * N = e
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;
x * N in Cosets N by GROUP_6:14;
hence contradiction by A2, A6, TARSKI:def 1; :: thesis: verum
end;
the carrier of N c= the carrier of H1 by GROUP_2:def 5;
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