let O be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( s1 is_equivalent_with s2 & s1 is jordan_holder implies s2 is jordan_holder )
assume A1: s1 is_equivalent_with s2 ; :: thesis: ( not s1 is jordan_holder or s2 is jordan_holder )
assume A2: s1 is jordan_holder ; :: thesis: s2 is jordan_holder

per cases ( len s1 <= 0 + 1 or len s1 > 1 ) ;

suppose A3: len s1 <= 0 + 1 ; :: thesis: s2 is jordan_holder

per cases ( len s1 = 0 or len s1 = 1 ) by A3, NAT_1:26;

suppose A4: len s1 = 0 ; :: thesis: s2 is jordan_holder

then A5: s1 = {} ;
len s2 = 0 by A1, A4, Def35;
then s2 = {} ;
hence s2 is jordan_holder by A2, A5; :: thesis: verum

end;

suppose A6: len s1 = 1 ; :: thesis: s2 is jordan_holder

then A7: s1 . 1 = (1). G by Def31;
A8: len s2 = 1 by A1, A6, Def35;
s1 = <*(s1 . 1)*> by A6, FINSEQ_1:57
.= <*(s2 . 1)*> by A7, A8, Def31
.= s2 by A8, FINSEQ_1:57 ;
hence s2 is jordan_holder by A2; :: thesis: verum

end;

end;

end;

suppose A9: len s1 > 1 ; :: thesis: s2 is jordan_holder

then A10: not s1 is empty ;
A11: len s2 > 1 by A1, A9, Def35;
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;
set f1 = the_series_of_quotients_of s1;
set f2 = the_series_of_quotients_of s2;
A13: ( len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) & ( for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom (the_series_of_quotients_of s1) & j = (p " ) . i & H1 = (the_series_of_quotients_of s1) . i & H2 = (the_series_of_quotients_of s2) . j holds
H1,H2 are_isomorphic ) ) by A12, Def37;

now

let j be Nat; :: thesis: ( j in dom (the_series_of_quotients_of s2) implies (the_series_of_quotients_of s2) . j is strict simple GroupWithOperators of O )
assume A14: j in dom (the_series_of_quotients_of s2) ; :: thesis: (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;
A15: dom (the_series_of_quotients_of s1) = Seg (len (the_series_of_quotients_of s1)) by FINSEQ_1:def 3
.= Seg (len (the_series_of_quotients_of s2)) by A12, Def37
.= dom (the_series_of_quotients_of s2) by FINSEQ_1:def 3 ;
then A16: p . j in dom (the_series_of_quotients_of s2) by A14, FUNCT_2:7;
then A17: p . j in Seg (len (the_series_of_quotients_of s2)) by FINSEQ_1:def 3;
reconsider i = p . j as Element of NAT by A16;
A18: i in dom (the_series_of_quotients_of s1) by A13, A17, FINSEQ_1:def 3;
then A19: (the_series_of_quotients_of s1) . i in rng (the_series_of_quotients_of s1) by FUNCT_1:12;
(the_series_of_quotients_of s2) . j in rng (the_series_of_quotients_of s2) by A14, FUNCT_1:12;
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 A19, Th102;
( i in dom (the_series_of_quotients_of s1) & j = (p " ) . i & H1 = (the_series_of_quotients_of s1) . i & H2 = (the_series_of_quotients_of s2) . j ) by A14, A15, FUNCT_2:7, FUNCT_2:32;
then A20: H1,H2 are_isomorphic by A12, Def37;
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 A20, Th82; :: thesis: verum

end;

hence s2 is jordan_holder by A11, Th110; :: thesis: verum

end;

end;