let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies ( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding ) )
assume a1: Rseq is nonnegative-yielding ; :: thesis: ( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding )
now :: thesis: for i, j being Nat holds
( (Partial_Sums_in_cod2 Rseq) . (i,j) >= 0 & (Partial_Sums_in_cod1 Rseq) . (i,j) >= 0 )
let i, j be Nat; :: thesis: ( (Partial_Sums_in_cod2 Rseq) . (i,j) >= 0 & (Partial_Sums_in_cod1 Rseq) . (i,j) >= 0 )
defpred S1[ Nat] means (Partial_Sums_in_cod2 Rseq) . (i,$1) >= 0 ;
(Partial_Sums_in_cod2 Rseq) . (i,0) = Rseq . (i,0) by DefCS;
then a2: S1[ 0 ] by a1;
a3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then a4: ( (Partial_Sums_in_cod2 Rseq) . (i,k) >= 0 & Rseq . (i,(k + 1)) >= 0 ) by a1;
(Partial_Sums_in_cod2 Rseq) . (i,(k + 1)) = ((Partial_Sums_in_cod2 Rseq) . (i,k)) + (Rseq . (i,(k + 1))) by DefCS;
hence S1[k + 1] by a4; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(a2, a3);
hence (Partial_Sums_in_cod2 Rseq) . (i,j) >= 0 ; :: thesis: (Partial_Sums_in_cod1 Rseq) . (i,j) >= 0
defpred S2[ Nat] means (Partial_Sums_in_cod1 Rseq) . ($1,j) >= 0 ;
(Partial_Sums_in_cod1 Rseq) . (0,j) = Rseq . (0,j) by DefRS;
then a5: S2[ 0 ] by a1;
a6: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then a7: ( (Partial_Sums_in_cod1 Rseq) . (k,j) >= 0 & Rseq . ((k + 1),j) >= 0 ) by a1;
(Partial_Sums_in_cod1 Rseq) . ((k + 1),j) = ((Partial_Sums_in_cod1 Rseq) . (k,j)) + (Rseq . ((k + 1),j)) by DefRS;
hence S2[k + 1] by a7; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(a5, a6);
hence (Partial_Sums_in_cod1 Rseq) . (i,j) >= 0 ; :: thesis: verum
end;
hence ( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding ) ; :: thesis: verum