let i be natural Number ; for R1, R2 being real-valued i -element FinSequence st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2
let R1, R2 be real-valued i -element FinSequence; ( ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 )
A0:
i is Nat
by TARSKI:1;
defpred S1[ Nat] means for R1, R2 being real-valued $1 -element FinSequence st ( for j being Nat st j in Seg $1 holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2;
A1:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A2:
for
R1,
R2 being
real-valued i -element FinSequence st ( for
j being
Nat st
j in Seg i holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2
;
S1[i + 1]
set n =
i + 1;
let R1,
R2 be
real-valued i + 1
-element FinSequence;
( ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 )
assume A3:
for
j being
Nat st
j in Seg (i + 1) holds
R1 . j <= R2 . j
;
Sum R1 <= Sum R2
R1 is
Element of
(i + 1) -tuples_on REAL
by Lm;
then consider R19 being
Element of
i -tuples_on REAL,
x1 being
Element of
REAL such that A4:
R1 = R19 ^ <*x1*>
by FINSEQ_2:117;
R2 is
Element of
(i + 1) -tuples_on REAL
by Lm;
then consider R29 being
Element of
i -tuples_on REAL,
x2 being
Element of
REAL such that A5:
R2 = R29 ^ <*x2*>
by FINSEQ_2:117;
for
j being
Nat st
j in Seg i holds
R19 . j <= R29 . j
then A8:
Sum R19 <= Sum R29
by A2;
A9:
R2 . (i + 1) = x2
by A5, FINSEQ_2:116;
R1 . (i + 1) = x1
by A4, FINSEQ_2:116;
then A10:
x1 <= x2
by A3, A9, FINSEQ_1:4;
A11:
Sum R2 = (Sum R29) + x2
by A5, Th74;
Sum R1 = (Sum R19) + x1
by A4, Th74;
hence
Sum R1 <= Sum R2
by A10, A8, A11, XREAL_1:7;
verum
end;
A12:
S1[ 0 ]
;
for i being Nat holds S1[i]
from NAT_1:sch 2(A12, A1);
hence
( ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 )
by A0; verum