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

now

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

end;

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

end;

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

end;

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

defpred S₁[ Nat] means for s1', s2' being CompositionSeries of G st not s1' is empty & not s2' is empty & len s1' = (len s1) + $1 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 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

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

now

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

end;

then A9: s1 is_finer_than s2 by Def32;
s1 is strictly_decreasing by A1, Def34;
hence contradiction by A2, A6, A8, A9, Def34; :: 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

let s1', s2' be CompositionSeries of G; :: thesis: ( not s1' is empty & not s2' is empty & len s1' = ((len s1) + n) + 1 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 implies S₁[n + 1] )
assume that
not s1' is empty and
not s2' is empty ; :: thesis: ( len s1' = ((len s1) + n) + 1 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 implies S₁[n + 1] )
assume A12: len s1' = ((len s1) + n) + 1 ; :: thesis: ( s1' is_finer_than s1 & s2' is_finer_than s2 & 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 implies S₁[n + 1] )
set f1 = the_series_of_quotients_of s1';
assume A13: s1' is_finer_than s1 ; :: thesis: ( s2' is_finer_than s2 & 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 implies S₁[n + 1] )
(n + 1) + (len s1) > 0 + (len s1) by XREAL_1:8;
then consider i being Nat such that
A14: i in dom (the_series_of_quotients_of s1') and
A15: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1') . i holds
H is trivial by A1, A12, A13, Th109;
reconsider s1'' = Del s1',i as FinSequence of the_stable_subgroups_of G by FINSEQ_3:114;
A16: i in dom s1' by A14, A15, Th103;
A17: ( i + 1 in dom s1' & s1' . i = s1' . (i + 1) ) by A14, A15, Th103;
then reconsider s1'' = s1'' as CompositionSeries of G by A16, Th94;
A18: the_series_of_quotients_of s1'' = Del (the_series_of_quotients_of s1'),i by A16, A17, Th104;
set f2 = the_series_of_quotients_of s2';
assume A19: s2' is_finer_than s2 ; :: 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 implies S₁[n + 1] )
given p being Permutation of dom (the_series_of_quotients_of s1') such that A20: the_series_of_quotients_of s1', the_series_of_quotients_of s2' are_equivalent_under p,O ; :: thesis: S₁[n + 1]
set H1 = (the_series_of_quotients_of s1') . i;
A21: (the_series_of_quotients_of s1') . i in rng (the_series_of_quotients_of s1') by A14, FUNCT_1:12;
set j = (p " ) . i;
reconsider j = (p " ) . i as Nat ;
set H2 = (the_series_of_quotients_of s2') . j;
reconsider s2'' = Del s2',j as FinSequence of the_stable_subgroups_of G by FINSEQ_3:114;
rng (p " ) c= dom (the_series_of_quotients_of s1') ;
then A22: rng (p " ) c= Seg (len (the_series_of_quotients_of s1')) by FINSEQ_1:def 3;
A23: len (the_series_of_quotients_of s1') = len (the_series_of_quotients_of s2') by A20, Def37;
(p " ) . i in rng (p " ) by A14, FUNCT_2:6;
then (p " ) . i in Seg (len (the_series_of_quotients_of s1')) by A22;
then A24: j in dom (the_series_of_quotients_of s2') by A23, FINSEQ_1:def 3;
then (the_series_of_quotients_of s2') . j in rng (the_series_of_quotients_of s2') by FUNCT_1:12;
then reconsider H1 = (the_series_of_quotients_of s1') . i, H2 = (the_series_of_quotients_of s2') . j as strict GroupWithOperators of O by A21, Th102;
A25: H1 is trivial by A15;
H1,H2 are_isomorphic by A20, A14, Def37;
then A26: for H being GroupWithOperators of O st H = (the_series_of_quotients_of s2') . j holds
H is trivial by A25, Th58;
then A27: ( j in dom s2' & j + 1 in dom s2' ) by A24, Th103;
A28: s2' . j = s2' . (j + 1) by A24, A26, Th103;
then reconsider s2'' = s2'' as CompositionSeries of G by A27, Th94;
A29: ( s2'' is_finer_than s2 & not s2'' is empty ) by A2, A7, A19, A27, A28, Th97, Th99;
A30: len s1'' = (len s1) + n by A12, A16, FINSEQ_3:118;
the_series_of_quotients_of s2'' = Del (the_series_of_quotients_of s2'),j by A27, A28, Th104;
then A31: 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 A20, A14, A18, Th106;
( s1'' is_finer_than s1 & not s1'' 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 s1', s2' be CompositionSeries of G; :: thesis: ( not s1' is empty & not s2' is empty & len s1' = (len s1) + 0 & s1' is_finer_than s1 & s2' is_finer_than s2 & 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 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 s1' is empty & not s2' is empty ) ; :: thesis: ( not len s1' = (len s1) + 0 or not s1' is_finer_than s1 or not s2' is_finer_than s2 or for p being Permutation of dom (the_series_of_quotients_of s1') holds not the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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 s1' = (len s1) + 0 & s1' is_finer_than s1 ) ; :: thesis: ( not s2' is_finer_than s2 or for p being Permutation of dom (the_series_of_quotients_of s1') holds not the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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: s2' is_finer_than s2 ; :: thesis: ( for p being Permutation of dom (the_series_of_quotients_of s1') holds not the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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 s1') such that A36: the_series_of_quotients_of s1', the_series_of_quotients_of s2' 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: s1' is_equivalent_with s2' by A33, A36, Th108;
s1' = s1 by A34, Th96;
then s2' is jordan_holder by A1, A37, Th115;
then s2' = s2 by A2, A35, Th98;
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 s1', s2' being CompositionSeries of G such that
A39: s1' is_finer_than s1 and
A40: s2' is_finer_than s2 and
A41: s1' is_equivalent_with s2' by Th118;
A42: not s1' is empty by A6, A39, Th97;
A43: ex n being Nat st len s1' = (len s1) + n by A39, Th95;
A44: not s2' is empty by A7, A40, Th97;
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 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;