let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies ( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) ) ) )
assume A1: Rseq is nonnegative-yielding ; :: thesis: ( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) ) )

hereby :: thesis: for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2)

let i1, i2, j be Nat; :: thesis: ( i1 <= i2 implies (Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) )
assume A3: i1 <= i2 ; :: thesis: (Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j)
defpred S₁[ Nat] means (Partial_Sums Rseq) . (i1,$1) <= (Partial_Sums Rseq) . (i2,$1);
( (Partial_Sums Rseq) . (i1,0) = (Partial_Sums_in_cod1 Rseq) . (i1,0) & (Partial_Sums Rseq) . (i2,0) = (Partial_Sums_in_cod1 Rseq) . (i2,0) ) by DefCS;
then A4: S₁[ 0 ] by A3, A1, th1003;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
A7: (Partial_Sums_in_cod1 Rseq) . (i1,(k + 1)) <= (Partial_Sums_in_cod1 Rseq) . (i2,(k + 1)) by A3, A1, th1003;
( (Partial_Sums Rseq) . (i1,(k + 1)) = ((Partial_Sums Rseq) . (i1,k)) + ((Partial_Sums_in_cod1 Rseq) . (i1,(k + 1))) & (Partial_Sums Rseq) . (i2,(k + 1)) = ((Partial_Sums Rseq) . (i2,k)) + ((Partial_Sums_in_cod1 Rseq) . (i2,(k + 1))) ) by DefCS;
hence S₁[k + 1] by A6, A7, XREAL_1:7; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
hence (Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) ; :: thesis: verum

end;

hereby :: thesis: verum

let i, j1, j2 be Nat; :: thesis: ( j1 <= j2 implies (Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) )
assume B3: j1 <= j2 ; :: thesis: (Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2)
defpred S₁[ Nat] means (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ($1,j1) <= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ($1,j2);
( (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,j1) = (Partial_Sums_in_cod2 Rseq) . (0,j1) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,j2) = (Partial_Sums_in_cod2 Rseq) . (0,j2) ) by DefRS;
then B4: S₁[ 0 ] by B3, A1, th1003;
B5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume C6: S₁[k] ; :: thesis: S₁[k + 1]
C7: (Partial_Sums_in_cod2 Rseq) . ((k + 1),j1) <= (Partial_Sums_in_cod2 Rseq) . ((k + 1),j2) by B3, A1, th1003;
( (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((k + 1),j1) = ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (k,j1)) + ((Partial_Sums_in_cod2 Rseq) . ((k + 1),j1)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((k + 1),j2) = ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (k,j2)) + ((Partial_Sums_in_cod2 Rseq) . ((k + 1),j2)) ) by DefRS;
hence S₁[k + 1] by C6, C7, XREAL_1:7; :: thesis: verum

end;

B6: for k being Nat holds S₁[k] from NAT_1:sch 2(B4, B5);
( (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (i,j1) = (Partial_Sums Rseq) . (i,j1) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (i,j2) = (Partial_Sums Rseq) . (i,j2) ) by th103;
hence (Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) by B6; :: thesis: verum

end;