let O be set ; :: thesis: for G being GroupWithOperators of O

for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds

s2 is_finer_than s1

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds

s2 is_finer_than s1

let s1, s2 be CompositionSeries of G; :: thesis: ( ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 implies s2 is_finer_than s1 )

assume A1: ( len s1 <= 1 or len s2 <= 1 ) ; :: thesis: ( not len s1 <= len s2 or s2 is_finer_than s1 )

assume A2: len s1 <= len s2 ; :: thesis: s2 is_finer_than s1

then A3: len s1 <= 1 by A1, XXREAL_0:2;

for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds

s2 is_finer_than s1

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds

s2 is_finer_than s1

let s1, s2 be CompositionSeries of G; :: thesis: ( ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 implies s2 is_finer_than s1 )

assume A1: ( len s1 <= 1 or len s2 <= 1 ) ; :: thesis: ( not len s1 <= len s2 or s2 is_finer_than s1 )

assume A2: len s1 <= len s2 ; :: thesis: s2 is_finer_than s1

then A3: len s1 <= 1 by A1, XXREAL_0:2;

per cases
( len s1 = 1 or len s1 <> 1 )
;

end;

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

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

end;now :: thesis: ex x being set st

( x c= dom s2 & s1 = s2 * (Sgm x) )

hence
s2 is_finer_than s1
; :: thesis: verum( x c= dom s2 & s1 = s2 * (Sgm x) )

reconsider D = Seg (len s2) as non empty set by A2, A4;

set x = {1};

take x = {1}; :: thesis: ( x c= dom s2 & s1 = s2 * (Sgm x) )

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: s1 = s2 * (Sgm x)

{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: verum

end;set x = {1};

take x = {1}; :: thesis: ( x c= dom s2 & s1 = s2 * (Sgm x) )

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: s1 = s2 * (Sgm x)

{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: verum

suppose
len s1 <> 1
; :: thesis: s2 is_finer_than s1

then
len s1 < 0 + 1
by A3, XXREAL_0:1;

then A7: s1 = {} by NAT_1:13;

end;then A7: s1 = {} by NAT_1:13;

now :: thesis: ex x being set st

( x c= dom s2 & s1 = s2 * (Sgm x) )

hence
s2 is_finer_than s1
; :: thesis: verum( 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 A7, FINSEQ_3:43; :: thesis: verum

end;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 A7, FINSEQ_3:43; :: thesis: verum