let Rseq be Function of [:NAT,NAT:],REAL; :: thesis:
assume A1: Rseq is nonnegative-yielding ; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:

X1: now :: thesis:

let i be Nat; :: thesis:
i is Element of NAT by ORDINAL1:def 12;
then A3: (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . i = (Partial_Sums_in_cod1 Rseq) . (i,k) by MESFUNC9:def 7;
(ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . (i + 1) = (Partial_Sums_in_cod1 Rseq) . ((i + 1),k) by MESFUNC9:def 7
.= ((Partial_Sums_in_cod1 Rseq) . (i,k)) + (Rseq . ((i + 1),k)) by DefRS ;
hence (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . i <= (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . (i + 1) by A1, A3, XREAL_1:31; :: thesis:

end;

hence ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is V115() by VALUED_1:def 15; :: thesis:

X2: now :: thesis:

let j be Nat; :: thesis:
j is Element of NAT by ORDINAL1:def 12;
then A5: (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . j = (Partial_Sums_in_cod2 Rseq) . (k,j) by MESFUNC9:def 6;
(ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . (j + 1) = (Partial_Sums_in_cod2 Rseq) . (k,(j + 1)) by MESFUNC9:def 6
.= ((Partial_Sums_in_cod2 Rseq) . (k,j)) + (Rseq . (k,(j + 1))) by DefCS ;
hence (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . (j + 1) by A1, A5, XREAL_1:31; :: thesis:

end;

hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is V115() by VALUED_1:def 15; :: thesis:
B1: (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . 0 = (Partial_Sums_in_cod1 Rseq) . (0,k) by MESFUNC9:def 7
.= Rseq . (0,k) by DefRS ;

now :: thesis:

let i be Nat; :: thesis:
(ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . (i + 0) >= (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . 0 by X1, SEQM_3:5, VALUED_1:def 15;
hence (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . i >= 0 by B1, A1; :: thesis:

end;

hence ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative ; :: thesis:
B2: (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . 0 = (Partial_Sums_in_cod2 Rseq) . (k,0) by MESFUNC9:def 6
.= Rseq . (k,0) by DefCS ;

now :: thesis:

let i be Nat; :: thesis:
(ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . (i + 0) >= (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . 0 by X2, SEQM_3:5, VALUED_1:def 15;
hence (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . i >= 0 by B2, A1; :: thesis:

end;

hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative ; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
B3: (ProjMap2 ((Partial_Sums_in_cod2 Rseq),k)) . i = (Partial_Sums_in_cod2 Rseq) . (i1,k) by MESFUNC9:def 7
.= (Partial_Sums (ProjMap1 (Rseq,i1))) . k by th100 ;
(ProjMap1 (Rseq,i1)) . k = Rseq . (i1,k) by MESFUNC9:def 6;
then B4: (ProjMap1 (Rseq,i1)) . k >= 0 by A1;

now :: thesis:

let p be Nat; :: thesis:
p is Element of NAT by ORDINAL1:def 12;
then (ProjMap1 (Rseq,i1)) . p = Rseq . (i1,p) by MESFUNC9:def 6;
hence (ProjMap1 (Rseq,i1)) . p >= 0 by A1; :: thesis:

end;

then ProjMap1 (Rseq,i1) is nonnegative-yielding ;
hence (ProjMap2 ((Partial_Sums_in_cod2 Rseq),k)) . i >= 0 by B3, B4, th101; :: thesis:

end;

hence ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative ; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
B5: (ProjMap1 ((Partial_Sums_in_cod1 Rseq),k)) . i = (Partial_Sums_in_cod1 Rseq) . (k,i1) by MESFUNC9:def 6
.= (Partial_Sums (ProjMap2 (Rseq,i1))) . k by th100 ;
(ProjMap2 (Rseq,i1)) . k = Rseq . (k,i1) by MESFUNC9:def 7;
then B6: (ProjMap2 (Rseq,i1)) . k >= 0 by A1;

now :: thesis:

let p be Nat; :: thesis:
p is Element of NAT by ORDINAL1:def 12;
then (ProjMap2 (Rseq,i1)) . p = Rseq . (p,i1) by MESFUNC9:def 7;
hence (ProjMap2 (Rseq,i1)) . p >= 0 by A1; :: thesis:

end;

then ProjMap2 (Rseq,i1) is nonnegative-yielding ;
hence (ProjMap1 ((Partial_Sums_in_cod1 Rseq),k)) . i >= 0 by B5, B6, th101; :: thesis:

end;

hence ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative ; :: thesis:

end;