let Rseq be Function of [:NAT,NAT:],REAL; ( 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
; ( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding )
now 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;
( (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]
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(a2, a3);
hence
(Partial_Sums_in_cod2 Rseq) . (
i,
j)
>= 0
;
(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]
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(a5, a6);
hence
(Partial_Sums_in_cod1 Rseq) . (
i,
j)
>= 0
;
verum end;
hence
( Partial_Sums_in_cod2 Rseq is nonnegative-yielding & Partial_Sums_in_cod1 Rseq is nonnegative-yielding )
; verum