let O be set ; :: thesis: for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds
s1 is_equivalent_with s2
let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds
s1 is_equivalent_with s2
let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is jordan_holder & s2 is jordan_holder implies s1 is_equivalent_with s2 )
assume A1: s1 is jordan_holder ; :: thesis: ( not s2 is jordan_holder or s1 is_equivalent_with s2 )
assume A2: s2 is jordan_holder ; :: thesis: s1 is_equivalent_with s2

per cases ( s1 is empty or not s1 is empty ) ;

suppose A3: s1 is empty ; :: thesis: s1 is_equivalent_with s2

now :: thesis: s2 is empty

now :: thesis: ex x being set st
( x c= dom s2 & s1 = s2 * (Sgm x) )

set x = {} ;
take x = {} ; :: thesis: ( x c= dom s2 & s1 = s2 * (Sgm x) )
thus x c= dom s2 ; :: thesis: s1 = s2 * (Sgm x)
thus s1 = s2 * (Sgm x) by A3, FINSEQ_3:43; :: thesis: verum

end;

then A4: s2 is_finer_than s1 ;
assume A5: not s2 is empty ; :: thesis: contradiction
s2 is strictly_decreasing by A2;
hence contradiction by A1, A3, A5, A4; :: thesis: verum

end;

hence s1 is_equivalent_with s2 by A3; :: thesis: verum

end;

suppose A6: not s1 is empty ; :: thesis: s1 is_equivalent_with s2

defpred S₁[ Nat] means for s19, s29 being CompositionSeries of G st not s19 is empty & not s29 is empty & len s19 = (len s1) + $1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O holds
ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O;

A7: now :: thesis: not s2 is empty

assume A8: s2 is empty ; :: thesis: contradiction

now :: thesis: ex x being set st
( x c= dom s1 & s2 = s1 * (Sgm x) )

set x = {} ;
take x = {} ; :: thesis: ( x c= dom s1 & s2 = s1 * (Sgm x) )
thus x c= dom s1 ; :: thesis: s2 = s1 * (Sgm x)
thus s2 = s1 * (Sgm x) by A8, FINSEQ_3:43; :: thesis: verum

end;

then A9: s1 is_finer_than s2 ;
s1 is strictly_decreasing by A1;
hence contradiction by A2, A6, A8, A9; :: thesis: verum

end;

A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A11: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: for s19, s29 being CompositionSeries of G st not s19 is empty & not s29 is empty & len s19 = ((len s1) + n) + 1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O holds
S₁[n + 1]

let s19, s29 be CompositionSeries of G; :: thesis: ( not s19 is empty & not s29 is empty & len s19 = ((len s1) + n) + 1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S₁[n + 1] )
assume that
not s19 is empty and
not s29 is empty ; :: thesis: ( len s19 = ((len s1) + n) + 1 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S₁[n + 1] )
assume A12: len s19 = ((len s1) + n) + 1 ; :: thesis: ( s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S₁[n + 1] )
set f1 = the_series_of_quotients_of s19;
assume A13: s19 is_finer_than s1 ; :: thesis: ( s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S₁[n + 1] )
(n + 1) + (len s1) > 0 + (len s1) by XREAL_1:6;
then consider i being Nat such that
A14: i in dom (the_series_of_quotients_of s19) and
A15: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s19) . i holds
H is trivial by A1, A12, A13, Th109;
reconsider s199 = Del (s19,i) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;
A16: i in dom s19 by A14, A15, Th103;
A17: ( i + 1 in dom s19 & s19 . i = s19 . (i + 1) ) by A14, A15, Th103;
then reconsider s199 = s199 as CompositionSeries of G by A16, Th94;
A18: the_series_of_quotients_of s199 = Del ((the_series_of_quotients_of s19),i) by A16, A17, Th104;
set f2 = the_series_of_quotients_of s29;
assume A19: s29 is_finer_than s2 ; :: thesis: ( ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies S₁[n + 1] )
given p being Permutation of (dom (the_series_of_quotients_of s19)) such that A20: the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O ; :: thesis: S₁[n + 1]
set H1 = (the_series_of_quotients_of s19) . i;
A21: (the_series_of_quotients_of s19) . i in rng (the_series_of_quotients_of s19) by A14, FUNCT_1:3;
set j = (p ") . i;
reconsider j = (p ") . i as Nat ;
set H2 = (the_series_of_quotients_of s29) . j;
reconsider s299 = Del (s29,j) as FinSequence of the_stable_subgroups_of G by FINSEQ_3:105;
rng (p ") c= dom (the_series_of_quotients_of s19) ;
then A22: rng (p ") c= Seg (len (the_series_of_quotients_of s19)) by FINSEQ_1:def 3;
A23: len (the_series_of_quotients_of s19) = len (the_series_of_quotients_of s29) by A20;
(p ") . i in rng (p ") by A14, FUNCT_2:4;
then (p ") . i in Seg (len (the_series_of_quotients_of s19)) by A22;
then A24: j in dom (the_series_of_quotients_of s29) by A23, FINSEQ_1:def 3;
then (the_series_of_quotients_of s29) . j in rng (the_series_of_quotients_of s29) by FUNCT_1:3;
then reconsider H1 = (the_series_of_quotients_of s19) . i, H2 = (the_series_of_quotients_of s29) . j as strict GroupWithOperators of O by A21, Th102;
A25: H1 is trivial by A15;
H1,H2 are_isomorphic by A20, A14;
then A26: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s29) . j holds
H is trivial by A25, Th58;
then A27: ( j in dom s29 & j + 1 in dom s29 ) by A24, Th103;
A28: s29 . j = s29 . (j + 1) by A24, A26, Th103;
then reconsider s299 = s299 as CompositionSeries of G by A27, Th94;
A29: ( s299 is_finer_than s2 & not s299 is empty ) by A2, A7, A19, A27, A28, Th97, Th99;
A30: len s199 = (len s1) + n by A12, A16, FINSEQ_3:109;
the_series_of_quotients_of s299 = Del ((the_series_of_quotients_of s29),j) by A27, A28, Th104;
then A31: ex p being Permutation of (dom (the_series_of_quotients_of s199)) st the_series_of_quotients_of s199, the_series_of_quotients_of s299 are_equivalent_under p,O by A20, A14, A18, Th106;
( s199 is_finer_than s1 & not s199 is empty ) by A1, A6, A13, A16, A17, Th97, Th99;
hence S₁[n + 1] by A11, A30, A29, A31; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A32: S₁[ 0 ]

proof

let s19, s29 be CompositionSeries of G; :: thesis: ( not s19 is empty & not s29 is empty & len s19 = (len s1) + 0 & s19 is_finer_than s1 & s29 is_finer_than s2 & ex p being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O implies ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )
assume A33: ( not s19 is empty & not s29 is empty ) ; :: thesis: ( not len s19 = (len s1) + 0 or not s19 is_finer_than s1 or not s29 is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )
assume A34: ( len s19 = (len s1) + 0 & s19 is_finer_than s1 ) ; :: thesis: ( not s29 is_finer_than s2 or for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )
assume A35: s29 is_finer_than s2 ; :: thesis: ( for p being Permutation of (dom (the_series_of_quotients_of s19)) holds not the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O or ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )
given p being Permutation of (dom (the_series_of_quotients_of s19)) such that A36: the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p,O ; :: thesis: ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O
A37: s19 is_equivalent_with s29 by A33, A36, Th108;
s19 = s1 by A34, Th96;
then s29 is jordan_holder by A1, A37, Th115;
then s29 = s2 by A2, A35;
then s1 is_equivalent_with s2 by A34, A37, Th96;
hence ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A6, A7, Th108; :: thesis: verum

end;

A38: for n being Nat holds S₁[n] from NAT_1:sch 2(A32, A10);
consider s19, s29 being CompositionSeries of G such that
A39: s19 is_finer_than s1 and
A40: s29 is_finer_than s2 and
A41: s19 is_equivalent_with s29 by Th118;
A42: not s19 is empty by A6, A39;
A43: ex n being Nat st len s19 = (len s1) + n by A39, Th95;
A44: not s29 is empty by A7, A40;
then ex p9 being Permutation of (dom (the_series_of_quotients_of s19)) st the_series_of_quotients_of s19, the_series_of_quotients_of s29 are_equivalent_under p9,O by A41, A42, Th108;
then ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O by A39, A40, A42, A44, A38, A43;
hence s1 is_equivalent_with s2 by A6, A7, Th108; :: thesis: verum

end;

end;