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 ;
suppose A6: len s1 = 1 ; :: thesis: s2 is jordan_holder
then A7: s1 . 1 = (1). G by Def28;
A8: len s2 = 1 by A1, A6;
s1 = <*(s1 . 1)*> by
.= <*(s2 . 1)*> by
.= s2 by ;
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;
then not s2 is empty ;
then consider p being Permutation of () such that
A12: the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by ;
A13: len = len by A12;
now :: thesis: for j being Nat st j in dom holds
. j is strict simple GroupWithOperators of O
let j be Nat; :: thesis: ( j in dom implies . j is strict simple GroupWithOperators of O )
set i = p . j;
set H1 = . (p . j);
set H2 = . j;
assume A14: j in dom ; :: thesis:
then A15: (the_series_of_quotients_of s2) . j in rng by FUNCT_1:3;
A16: dom = Seg () by FINSEQ_1:def 3
.= dom by ;
then A17: p . j in dom by ;
then reconsider i = p . j as Element of NAT ;
p . j in Seg () by ;
then A18: i in dom by ;
then (the_series_of_quotients_of s1) . i in rng by FUNCT_1:3;
then reconsider H1 = . (p . j), H2 = . j as strict GroupWithOperators of O by ;
( i in dom & j = (p ") . i ) by ;
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 ; :: thesis: verum
end;
hence s2 is jordan_holder by ; :: thesis: verum
end;
end;