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:25;

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

then len s2 = 0 by A1, Def35;
then A5: s2 = {} ;
s1 = {} by A4;
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:40
.= <*(s2 . 1)*> by A7, A8, Def31
.= s2 by A8, FINSEQ_1:40 ;
hence s2 is jordan_holder by A2; :: thesis: verum

end;

end;

end;

suppose A9: len s1 > 1 ; :: thesis: 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, 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;
A13: len (the_series_of_quotients_of s1) = len (the_series_of_quotients_of s2) 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 )
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) ; :: thesis: (the_series_of_quotients_of s2) . j is strict simple GroupWithOperators of O
then 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
.= Seg (len (the_series_of_quotients_of s2)) by A12, Def37
.= dom (the_series_of_quotients_of s2) by FINSEQ_1:def 3 ;
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, 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 A19, Th82; :: thesis: verum

end;

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

end;

end;