let p be FinSequence of NAT ; for i, j being Nat st i <= j holds
Sum (p | i) <= Sum (p | j)
let i, j be Nat; ( i <= j implies Sum (p | i) <= Sum (p | j) )
assume A1:
i <= j
; 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
;
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 for n being Nat st n in dom (p | i) holds
(p | i) . n = q . nreconsider p1 =
p as
FinSequence of
REAL by FINSEQ_2:24, NUMBERS:19;
let n be
Nat;
( n in dom (p | i) implies (p | i) . n = q . n )assume A10:
n in dom (p | i)
;
(p | i) . n = q . nthen 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
;
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;
verum end; end;