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) by Def32;
A3: x c= Seg (len s1) by A1, FINSEQ_1:def 3;
reconsider x = x as finite set by A1;

now

let y1 be set ; :: 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;

then dom s2 c= dom s1 by TARSKI:def 3;
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