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 ) & ex j being Nat st
( j in Seg i & 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 ) & ex j being Nat st
( j in Seg i & 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 ) & ex j being Nat st
( j in Seg $1 & R1 . j < R2 . j ) holds
Sum R1 < Sum R2;
now :: thesis: for i being Nat st S1[i] holds
for R1, R2 being real-valued b1 + 1 -element FinSequence st ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) holds
Sum R1 < Sum R2
let i be Nat; :: thesis: ( S1[i] implies for R1, R2 being real-valued i + 1 -element FinSequence st ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) holds
Sum R1 < Sum R2 )
assume A1: S1[i] ; :: thesis: for R1, R2 being real-valued i + 1 -element FinSequence st ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) holds
Sum R1 < Sum R2
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 ) & ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) implies Sum R1 < Sum R2 )
assume A2: for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ; :: thesis: ( ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) implies Sum R1 < Sum R2 )
given j being Nat such that A3: j in Seg (i + 1) and
A4: 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
A5: 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
A6: R2 = R29 ^ <*x2*> by FINSEQ_2:117;
A7: 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 A8: 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 A9: R29 . j = R2 . j by A6, A8, 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 A5, A8, FINSEQ_1:def 7;
hence R19 . j <= R29 . j by A2, A8, A9, FINSEQ_2:8; :: thesis: verum
end;
A10: R2 . (i + 1) = x2 by A6, FINSEQ_2:116;
A11: R1 . (i + 1) = x1 by A5, FINSEQ_2:116;
now :: thesis: Sum R1 < Sum R2
per cases ( j in Seg i or j = i + 1 ) by A3, FINSEQ_2:7;
suppose A12: j in Seg i ; :: thesis: Sum R1 < Sum R2
( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def 7, FINSEQ_1:def 3;
then A13: R29 . j = R2 . j by A6, A12, FINSEQ_1:def 7;
A14: ( Sum R1 = (Sum R19) + x1 & Sum R2 = (Sum R29) + x2 ) by A5, A6, Th74;
A15: x1 <= x2 by A2, A11, A10, FINSEQ_1:4;
( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def 7, FINSEQ_1:def 3;
then R19 . j = R1 . j by A5, A12, FINSEQ_1:def 7;
then Sum R19 < Sum R29 by A1, A4, A7, A12, A13;
hence Sum R1 < Sum R2 by A14, A15, XREAL_1:8; :: thesis: verum
end;
suppose A16: j = i + 1 ; :: thesis: Sum R1 < Sum R2
A17: Sum R2 = (Sum R29) + x2 by A6, Th74;
( Sum R19 <= Sum R29 & Sum R1 = (Sum R19) + x1 ) by A5, A7, Th74, Th82;
hence Sum R1 < Sum R2 by A4, A11, A10, A16, A17, XREAL_1:8; :: thesis: verum
end;
end;
end;
hence Sum R1 < Sum R2 ; :: thesis: verum
end;
then A18: for i being Nat st S1[i] holds
S1[i + 1] ;
A19: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch 2(A19, A18);
 hence ( ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg i & R1 . j < R2 . j ) implies Sum R1 < Sum R2 ) by A0; :: thesis: verum