for R1, R2 being real-valued FinSequence st 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 ) holds
Sum R1 < Sum R2