let i be natural Number ; :: thesis: 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; :: thesis: ( ( 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; :: thesis: ( 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 ; :: thesis: S1[i + 1]
set n = i + 1;
let R1, R2 be real-valued i + 1 -element FinSequence; :: thesis: ( ( 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 ; :: thesis: 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
proof
let j be Nat; :: thesis: ( j in Seg i implies R19 . j <= R29 . j )
assume A6: j in Seg i ; :: thesis: R19 . j <= R29 . j
( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def 7, FINSEQ_1:def 3;
then A7: R29 . j = R2 . j by A5, A6, FINSEQ_1:def 7;
( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def 7, FINSEQ_1:def 3;
then R19 . j = R1 . j by A4, A6, FINSEQ_1:def 7;
hence R19 . j <= R29 . j by A3, A6, A7, FINSEQ_2:8; :: thesis: verum
end;
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; :: thesis: 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; :: thesis: verum