let p be natural-valued FinSequence; :: thesis: for i, j being Nat st i <= j holds
Sum (p | i) <= Sum (p | j)
let i, j be Nat; :: thesis: ( i <= j implies Sum (p | i) <= Sum (p | j) )
assume A1: i <= j ; :: thesis: Sum (p | i) <= Sum (p | j)
then consider k being Nat such that
A2: j = i + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
reconsider p = p as FinSequence of NAT by FINSEQ_1:103;

per cases ( j <= len p or j > len p ) ;

suppose A3: j <= len p ; :: thesis: Sum (p | i) <= Sum (p | j)

then A4: len (p | j) = i + k by A2, FINSEQ_1:59;
then consider q, r being FinSequence of NAT such that
A5: len q = i and
len r = k and
A6: p | j = q ^ r by FINSEQ_2:23;
A7: len (p | i) = i by A1, A3, FINSEQ_1:59, XXREAL_0:2;
then A8: dom (p | i) = Seg i by FINSEQ_1:def 3;

A9: now :: thesis: for n being Nat st n in dom (p | i) holds
(p | i) . n = q . n

let n be Nat; :: thesis: ( n in dom (p | i) implies (p | i) . n = q . n )
assume A10: n in dom (p | i) ; :: thesis: (p | i) . n = q . n
then A11: (p | i) /. n = p /. n by FINSEQ_4:70;
A12: Seg i = dom q by A5, FINSEQ_1:def 3;
A13: ( Seg i c= Seg j & Seg j = dom (p | j) ) by A1, A2, A4, FINSEQ_1:5, FINSEQ_1:def 3;
Seg i = dom (p | i) by A7, FINSEQ_1:def 3;
then A14: (p | j) /. n = p /. n by A10, A13, FINSEQ_4:70;
thus (p | i) . n = (p | i) /. n by A10, PARTFUN1:def 6
.= (p | j) . n by A8, A10, A13, A11, A14, PARTFUN1:def 6
.= q . n by A6, A8, A10, A12, FINSEQ_1:def 7 ; :: thesis: verum

end;

A15: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6;
Sum (p | j) = (Sum q) + (Sum r) by A6, RVSUM_1:75;
hence Sum (p | i) <= Sum (p | j) by A7, A5, A9, A15, FINSEQ_2:9; :: thesis: verum

end;

suppose j > len p ; :: thesis: Sum (p | i) <= Sum (p | j)

then A16: p | j = p by FINSEQ_1:58;

now :: thesis: Sum (p | i) <= Sum (p | j)

per cases ( i >= len p or i < len p ) ;

suppose i >= len p ; :: thesis: Sum (p | i) <= Sum (p | j)

hence Sum (p | i) <= Sum (p | j) by A16, FINSEQ_1:58; :: thesis: verum

end;

suppose A17: i < len p ; :: thesis: Sum (p | i) <= Sum (p | j)

then consider t being Nat such that
A18: len p = i + t by NAT_1:10;
consider q, r being FinSequence of NAT such that
A19: len q = i and
len r = t and
A20: p = q ^ r by A18, FINSEQ_2:23;
A21: len (p | i) = i by A17, FINSEQ_1:59;
then A22: dom (p | i) = Seg i by FINSEQ_1:def 3;

A23: now :: thesis: for n being Nat st n in dom (p | i) holds
(p | i) . n = q . n

A24: Seg i = dom q by A19, FINSEQ_1:def 3;
let n be Nat; :: thesis: ( n in dom (p | i) implies (p | i) . n = q . n )
A25: dom (p | i) c= dom p by FINSEQ_5:18;
assume A26: n in dom (p | i) ; :: thesis: (p | i) . n = q . n
then A27: (p | i) /. n = p /. n by FINSEQ_4:70;
thus (p | i) . n = (p | i) /. n by A26, PARTFUN1:def 6
.= p . n by A26, A27, A25, PARTFUN1:def 6
.= q . n by A20, A22, A26, A24, FINSEQ_1:def 7 ; :: thesis: verum

end;

A28: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6;
Sum p = (Sum q) + (Sum r) by A20, RVSUM_1:75;
hence Sum (p | i) <= Sum (p | j) by A16, A19, A21, A23, A28, FINSEQ_2:9; :: thesis: verum

end;

end;

end;

hence Sum (p | i) <= Sum (p | j) ; :: thesis: verum

end;

end;