let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies for i1, i2, j1, j2 being Nat st i1 <= i2 & j1 <= j2 holds
(Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2) )
assume A1: Rseq is nonnegative-yielding ; :: thesis: for i1, i2, j1, j2 being Nat st i1 <= i2 & j1 <= j2 holds
(Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2)
hereby :: thesis: verum
let i1, i2, j1, j2 be Nat; :: thesis: ( i1 <= i2 & j1 <= j2 implies (Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2) )
assume ( i1 <= i2 & j1 <= j2 ) ; :: thesis: (Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2)
then ( (Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i1,j2) & (Partial_Sums Rseq) . (i1,j2) <= (Partial_Sums Rseq) . (i2,j2) ) by A1, th105;
hence (Partial_Sums Rseq) . (i1,j1) <= (Partial_Sums Rseq) . (i2,j2) by XXREAL_0:2; :: thesis: verum
end;