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;

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 )
;

end;

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;

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;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

A15:
(Sum q) + (Sum r) >= (Sum q) + 0
by XREAL_1:6;(p | i) . n = q . n

reconsider p1 = p as FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;

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;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

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

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

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

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

hence
Sum (p | i) <= Sum (p | j)
; :: thesis: verumper cases
( i >= len p or i < len p )
;

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;

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;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

A28:
(Sum q) + (Sum r) >= (Sum q) + 0
by XREAL_1:6;(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;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

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