let p be FinSequence of NAT ; :: 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;
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 ;
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 ;
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
reconsider p1 = p as FinSequence of REAL by ;
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 ;
A13: ( Seg i c= Seg j & Seg j = dom (p | j) ) by ;
Seg i = dom (p | i) by ;
then A14: (p | j) /. n = p /. n by ;
thus (p | i) . n = (p | i) /. n by
.= (p | j) . n by
.= q . n by ; :: thesis: verum
end;
A15: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6;
Sum (p | j) = (Sum q) + (Sum r) by ;
hence Sum (p | i) <= Sum (p | j) by ; :: 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 ; :: 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 ;
A21: len (p | i) = i by ;
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 ;
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
.= p . n by
.= q . n by ; :: thesis: verum
end;
A28: (Sum q) + (Sum r) >= (Sum q) + 0 by XREAL_1:6;
Sum p = (Sum q) + (Sum r) by ;
hence Sum (p | i) <= Sum (p | j) by ; :: thesis: verum
end;
end;
end;
hence Sum (p | i) <= Sum (p | j) ; :: thesis: verum
end;
end;