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

for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds

ex n being Nat st len s1 = (len s2) + n

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds

ex n being Nat st len s1 = (len s2) + n

let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is_finer_than s2 implies ex n being Nat st len s1 = (len s2) + n )

set n = (len s1) - (len s2);

assume s1 is_finer_than s2 ; :: thesis: ex n being Nat st len s1 = (len s2) + n

then consider x being set such that

A1: x c= dom s1 and

A2: s2 = s1 * (Sgm x) ;

A3: x c= Seg (len s1) by A1, FINSEQ_1:def 3;

reconsider x = x as finite set by A1;

then Seg (len s2) c= dom s1 by FINSEQ_1:def 3;

then Seg (len s2) c= Seg (len s1) by FINSEQ_1:def 3;

then len s2 <= len s1 by FINSEQ_1:5;

then (len s2) - (len s2) <= (len s1) - (len s2) by XREAL_1:9;

then (len s1) - (len s2) in NAT by INT_1:3;

then reconsider n = (len s1) - (len s2) as Nat ;

take n ; :: thesis: len s1 = (len s2) + n

thus len s1 = (len s2) + n ; :: thesis: verum

for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds

ex n being Nat st len s1 = (len s2) + n

let G be GroupWithOperators of O; :: thesis: for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds

ex n being Nat st len s1 = (len s2) + n

let s1, s2 be CompositionSeries of G; :: thesis: ( s1 is_finer_than s2 implies ex n being Nat st len s1 = (len s2) + n )

set n = (len s1) - (len s2);

assume s1 is_finer_than s2 ; :: thesis: ex n being Nat st len s1 = (len s2) + n

then consider x being set such that

A1: x c= dom s1 and

A2: s2 = s1 * (Sgm x) ;

A3: x c= Seg (len s1) by A1, FINSEQ_1:def 3;

reconsider x = x as finite set by A1;

now :: thesis: for y1 being object st y1 in dom s2 holds

y1 in dom s1

then
dom s2 c= dom s1
;y1 in dom s1

let y1 be object ; :: thesis: ( y1 in dom s2 implies y1 in dom s1 )

assume y1 in dom s2 ; :: thesis: y1 in dom s1

then y1 in dom (Sgm x) by A2, FUNCT_1:11;

then A4: y1 in Seg (card x) by A3, FINSEQ_3:40;

card x <= card (dom s1) by A1, NAT_1:43;

then Seg (card x) c= Seg (card (dom s1)) by FINSEQ_1:5;

then y1 in Seg (card (dom s1)) by A4;

then y1 in Seg (card (Seg (len s1))) by FINSEQ_1:def 3;

then y1 in Seg (len s1) by FINSEQ_1:57;

hence y1 in dom s1 by FINSEQ_1:def 3; :: thesis: verum

end;assume y1 in dom s2 ; :: thesis: y1 in dom s1

then y1 in dom (Sgm x) by A2, FUNCT_1:11;

then A4: y1 in Seg (card x) by A3, FINSEQ_3:40;

card x <= card (dom s1) by A1, NAT_1:43;

then Seg (card x) c= Seg (card (dom s1)) by FINSEQ_1:5;

then y1 in Seg (card (dom s1)) by A4;

then y1 in Seg (card (Seg (len s1))) by FINSEQ_1:def 3;

then y1 in Seg (len s1) by FINSEQ_1:57;

hence y1 in dom s1 by FINSEQ_1:def 3; :: thesis: verum

then Seg (len s2) c= dom s1 by FINSEQ_1:def 3;

then Seg (len s2) c= Seg (len s1) by FINSEQ_1:def 3;

then len s2 <= len s1 by FINSEQ_1:5;

then (len s2) - (len s2) <= (len s1) - (len s2) by XREAL_1:9;

then (len s1) - (len s2) in NAT by INT_1:3;

then reconsider n = (len s1) - (len s2) as Nat ;

take n ; :: thesis: len s1 = (len s2) + n

thus len s1 = (len s2) + n ; :: thesis: verum