theorem Th82: :: RVSUM_1:82

for i being natural Number
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 ) holds
Sum R1 <= Sum R2