let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let s1, s2 be CompositionSeries of G; :: thesis:
assume A1: ( len s1 <= 1 or len s2 <= 1 ) ; :: thesis:
assume A2: len s1 <= len s2 ; :: thesis:
then A3: len s1 <= 1 by A1, XXREAL_0:2;

suppose A4: len s1 = 1 ; :: thesis:

then A5: s1 = <*(s1 . 1)*> by FINSEQ_1:40;

reconsider D = Seg (len s2) as non empty set by A2, A4;
set x = {1};
take x = {1}; :: thesis:
set f = s2;
set p = <*1*>;
( dom s2 = Seg (len s2) & rng s2 c= the_stable_subgroups_of G ) by FINSEQ_1:def 3;
then reconsider f = s2 as Function of D,(the_stable_subgroups_of G) by FUNCT_2:2;
A6: 1 in Seg (len s2) by A2, A4;
then 1 in dom s2 by FINSEQ_1:def 3;
hence x c= dom s2 by ZFMISC_1:31; :: thesis:
{1} c= D by A6, ZFMISC_1:31;
then rng <*1*> c= D by FINSEQ_1:38;
then reconsider p = <*1*> as FinSequence of D by FINSEQ_1:def 4;
( Sgm x = p & f * p = <*(f . 1)*> ) by FINSEQ_2:35, FINSEQ_3:44;
then s2 * (Sgm x) = <*((Omega). G)*> by Def28;
hence s1 = s2 * (Sgm x) by A5, Def28; :: thesis:

end;

hence s2 is_finer_than s1 ; :: thesis:

end;

suppose len s1 <> 1 ; :: thesis:

then len s1 < 0 + 1 by A3, XXREAL_0:1;
then A7: s1 = {} by NAT_1:13;

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

end;

hence s2 is_finer_than s1 ; :: thesis:

end;

end;