let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies for k being Element of NAT holds
( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is non-decreasing & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is non-decreasing & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative ) )
assume A1: Rseq is nonnegative-yielding ; :: thesis: for k being Element of NAT holds
( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is non-decreasing & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is non-decreasing & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is non-decreasing & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is non-decreasing & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )

X1: now :: thesis: for i being Nat holds (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . i <= (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . (i + 1)

let i be Nat; :: thesis: (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . i <= (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . (i + 1)
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: verum

end;

hence ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is non-decreasing by VALUED_1:def 15; :: thesis: ( ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is non-decreasing & ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )

X2: now :: thesis: for j being Nat holds (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . (j + 1)

let j be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . j <= (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . (j + 1)
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: verum

end;

hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is non-decreasing by VALUED_1:def 15; :: thesis: ( ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )
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: for i being Nat holds (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . i >= 0

let i be Nat; :: thesis: (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . i >= 0
(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: verum

end;

hence ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative ; :: thesis: ( ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap2 ((Partial_Sums_in_cod2 Rseq),k) is nonnegative & ProjMap1 ((Partial_Sums_in_cod1 Rseq),k) is nonnegative )
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: for i being Nat holds (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . i >= 0

let i be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . i >= 0
(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: verum

end;

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

now :: thesis: for i being Nat holds (ProjMap2 ((Partial_Sums_in_cod2 Rseq),k)) . i >= 0

let i be Nat; :: thesis: (ProjMap2 ((Partial_Sums_in_cod2 Rseq),k)) . i >= 0
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: for p being Nat holds (ProjMap1 (Rseq,i1)) . p >= 0

let p be Nat; :: thesis: (ProjMap1 (Rseq,i1)) . p >= 0
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: verum

end;

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

end;

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

now :: thesis: for i being Nat holds (ProjMap1 ((Partial_Sums_in_cod1 Rseq),k)) . i >= 0

let i be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod1 Rseq),k)) . i >= 0
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: for p being Nat holds (ProjMap2 (Rseq,i1)) . p >= 0

let p be Nat; :: thesis: (ProjMap2 (Rseq,i1)) . p >= 0
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: verum

end;

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

end;

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

end;