let R1, R2 be real-valued FinSequence; :: thesis: ( len R1 = len R2 & ( for j being Nat st j in Seg (len R1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (len R1) & R1 . j < R2 . j ) implies Sum R1 < Sum R2 )
set i = len R1;
assume A1: ( len R1 = len R2 & ( for j being Nat st j in Seg (len R1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (len R1) & R1 . j < R2 . j ) ) ; :: thesis: Sum R1 < Sum R2
reconsider w = len R1 as natural Number ;
( R1 is FinSequence of REAL & R2 is FinSequence of REAL ) by RVSUM_1:145;
then reconsider r1 = R1, r2 = R2 as Element of w -tuples_on REAL by A1, FINSEQ_2:92;
Sum r1 < Sum r2 by A1, RVSUM_1:83;
hence Sum R1 < Sum R2 ; :: thesis: verum