let i be Nat; :: thesis: for R1, R2 being Element of i -tuples_on REAL 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 Element of i -tuples_on REAL ; :: 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 )
defpred S₁[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL 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;
A1: S₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

now

let i be Nat; :: thesis: ( S₁[i] implies for R1, R2 being Element of (i + 1) -tuples_on REAL 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 A3: S₁[i] ; :: thesis: for R1, R2 being Element of (i + 1) -tuples_on REAL 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 Element of (i + 1) -tuples_on REAL ; :: 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 A4: 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 A5: ( j in Seg (i + 1) & R1 . j < R2 . j ) ; :: thesis: Sum R1 < Sum R2
consider R1' being Element of i -tuples_on REAL , x1 being Element of REAL such that
A6: R1 = R1' ^ <*x1*> by FINSEQ_2:137;
consider R2' being Element of i -tuples_on REAL , x2 being Element of REAL such that
A7: R2 = R2' ^ <*x2*> by FINSEQ_2:137;
A8: ( i + 1 in Seg (i + 1) & R1 . (i + 1) = x1 & R2 . (i + 1) = x2 ) by A6, A7, FINSEQ_1:6, FINSEQ_2:136;
A9: for j being Nat st j in Seg i holds
R1' . j <= R2' . j

proof

let j be Nat; :: thesis: ( j in Seg i implies R1' . j <= R2' . j )
assume A10: j in Seg i ; :: thesis: R1' . j <= R2' . j
( Seg (len R1') = dom R1' & Seg (len R2') = dom R2' & len R1' = i & len R2' = i ) by FINSEQ_1:def 3, FINSEQ_1:def 18;
then ( j in Seg (i + 1) & R1' . j = R1 . j & R2' . j = R2 . j ) by A6, A7, A10, FINSEQ_1:def 7, FINSEQ_2:9;
hence R1' . j <= R2' . j by A4; :: thesis: verum

end;

now

per cases ( j in Seg i or j = i + 1 ) by A5, FINSEQ_2:8;

suppose A11: j in Seg i ; :: thesis: Sum R1 < Sum R2

( Seg (len R1') = dom R1' & Seg (len R2') = dom R2' & len R1' = i & len R2' = i ) by FINSEQ_1:def 3, FINSEQ_1:def 18;
then ( R1' . j = R1 . j & R2' . j = R2 . j ) by A6, A7, A11, FINSEQ_1:def 7;
then ( Sum R1' < Sum R2' & Sum R1 = (Sum R1') + x1 & Sum R2 = (Sum R2') + x2 & x1 <= x2 ) by A3, A4, A5, A6, A7, A8, A9, A11, Th104;
hence Sum R1 < Sum R2 by XREAL_1:10; :: thesis: verum

end;

suppose A12: j = i + 1 ; :: thesis: Sum R1 < Sum R2

( Sum R1' <= Sum R2' & Sum R1 = (Sum R1') + x1 & Sum R2 = (Sum R2') + x2 ) by A6, A7, A9, Th104, Th112;
hence Sum R1 < Sum R2 by A5, A8, A12, XREAL_1:10; :: thesis: verum

end;

end;

end;

hence Sum R1 < Sum R2 ; :: thesis: verum

end;

hence for i being Nat st S₁[i] holds
S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A2);
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 ) ; :: thesis: verum