let O be set ; for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_equivalent_with s2 & s1 is jordan_holder holds
s2 is jordan_holder
let G be GroupWithOperators of O; for s1, s2 being CompositionSeries of G st s1 is_equivalent_with s2 & s1 is jordan_holder holds
s2 is jordan_holder
let s1, s2 be CompositionSeries of G; ( s1 is_equivalent_with s2 & s1 is jordan_holder implies s2 is jordan_holder )
assume A1:
s1 is_equivalent_with s2
; ( not s1 is jordan_holder or s2 is jordan_holder )
assume A2:
s1 is jordan_holder
; s2 is jordan_holder
per cases
( len s1 <= 0 + 1 or len s1 > 1 )
;
suppose A9:
len s1 > 1
;
s2 is jordan_holder set f2 =
the_series_of_quotients_of s2;
set f1 =
the_series_of_quotients_of s1;
A10:
not
s1 is
empty
by A9;
A11:
len s2 > 1
by A1, A9;
then
not
s2 is
empty
;
then consider p being
Permutation of
(dom (the_series_of_quotients_of s1)) such that A12:
the_series_of_quotients_of s1,
the_series_of_quotients_of s2 are_equivalent_under p,
O
by A1, A10, Th108;
A13:
len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2)
by A12;
now for j being Nat st j in dom (the_series_of_quotients_of s2) holds
(the_series_of_quotients_of s2) . j is strict simple GroupWithOperators of Olet j be
Nat;
( j in dom (the_series_of_quotients_of s2) implies (the_series_of_quotients_of s2) . j is strict simple GroupWithOperators of O )set i =
p . j;
set H1 =
(the_series_of_quotients_of s1) . (p . j);
set H2 =
(the_series_of_quotients_of s2) . j;
assume A14:
j in dom (the_series_of_quotients_of s2)
;
(the_series_of_quotients_of s2) . j is strict simple GroupWithOperators of Othen A15:
(the_series_of_quotients_of s2) . j in rng (the_series_of_quotients_of s2)
by FUNCT_1:3;
A16:
dom (the_series_of_quotients_of s1) =
Seg (len (the_series_of_quotients_of s1))
by FINSEQ_1:def 3
.=
dom (the_series_of_quotients_of s2)
by FINSEQ_1:def 3, A12
;
then A17:
p . j in dom (the_series_of_quotients_of s2)
by A14, FUNCT_2:5;
then reconsider i =
p . j as
Element of
NAT ;
p . j in Seg (len (the_series_of_quotients_of s2))
by A17, FINSEQ_1:def 3;
then A18:
i in dom (the_series_of_quotients_of s1)
by A13, FINSEQ_1:def 3;
then
(the_series_of_quotients_of s1) . i in rng (the_series_of_quotients_of s1)
by FUNCT_1:3;
then reconsider H1 =
(the_series_of_quotients_of s1) . (p . j),
H2 =
(the_series_of_quotients_of s2) . j as
strict GroupWithOperators of
O by A15, Th102;
(
i in dom (the_series_of_quotients_of s1) &
j = (p ") . i )
by A14, A16, FUNCT_2:5, FUNCT_2:26;
then A19:
H1,
H2 are_isomorphic
by A12;
H1 is
strict simple GroupWithOperators of
O
by A2, A9, A18, Th110;
hence
(the_series_of_quotients_of s2) . j is
strict simple GroupWithOperators of
O
by A19, Th82;
verum end; hence
s2 is
jordan_holder
by A11, Th110;
verum end; end;