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

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 )
;

end;

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

end;

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

end;

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

then
len s2 = 0
by A1;

then A5: s2 = {} ;

s1 = {} by A4;

hence s2 is jordan_holder by A2, A5; :: thesis: verum

end;then A5: s2 = {} ;

s1 = {} by A4;

hence s2 is jordan_holder by A2, A5; :: thesis: verum

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 A6, FINSEQ_1:40

.= <*(s2 . 1)*> by A7, A8, Def28

.= s2 by A8, FINSEQ_1:40 ;

hence s2 is jordan_holder by A2; :: thesis: verum

end;A8: len s2 = 1 by A1, A6;

s1 = <*(s1 . 1)*> by A6, FINSEQ_1:40

.= <*(s2 . 1)*> by A7, A8, Def28

.= s2 by A8, FINSEQ_1:40 ;

hence s2 is jordan_holder by A2; :: thesis: verum

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 (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;

end;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 :: thesis: 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 O

hence
s2 is jordan_holder
by A11, Th110; :: thesis: verum(the_series_of_quotients_of s2) . j is strict simple GroupWithOperators of O

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

.= 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; :: thesis: verum

end;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

.= 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; :: thesis: verum