let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies for m, n being Nat holds
( Rseq . (m,n) <= (Partial_Sums_in_cod1 Rseq) . (m,n) & Rseq . (m,n) <= (Partial_Sums_in_cod2 Rseq) . (m,n) ) )
assume a1: Rseq is nonnegative-yielding ; :: thesis: for m, n being Nat holds
( Rseq . (m,n) <= (Partial_Sums_in_cod1 Rseq) . (m,n) & Rseq . (m,n) <= (Partial_Sums_in_cod2 Rseq) . (m,n) )
hereby :: thesis: verum
let m1, n1 be Nat; :: thesis: ( Rseq . (m1,n1) <= (Partial_Sums_in_cod1 Rseq) . (m1,n1) & Rseq . (m1,n1) <= (Partial_Sums_in_cod2 Rseq) . (m1,n1) )
reconsider m = m1, n = n1 as Element of NAT by ORDINAL1:def 12;
now :: thesis: for j being Nat holds (ProjMap2 (Rseq,n)) . j >= 0
let j be Nat; :: thesis: (ProjMap2 (Rseq,n)) . j >= 0
j in NAT by ORDINAL1:def 12;
then (ProjMap2 (Rseq,n)) . j = Rseq . (j,n) by MESFUNC9:def 7;
hence (ProjMap2 (Rseq,n)) . j >= 0 by a1; :: thesis: verum
end;
then (ProjMap2 (Rseq,n)) . m <= (Partial_Sums (ProjMap2 (Rseq,n))) . m by th101, RINFSUP1:def 3;
then (ProjMap2 (Rseq,n)) . m <= (Partial_Sums_in_cod1 Rseq) . (m,n) by th100;
hence Rseq . (m1,n1) <= (Partial_Sums_in_cod1 Rseq) . (m1,n1) by MESFUNC9:def 7; :: thesis: Rseq . (m1,n1) <= (Partial_Sums_in_cod2 Rseq) . (m1,n1)
now :: thesis: for j being Nat holds (ProjMap1 (Rseq,m)) . j >= 0
let j be Nat; :: thesis: (ProjMap1 (Rseq,m)) . j >= 0
j in NAT by ORDINAL1:def 12;
then (ProjMap1 (Rseq,m)) . j = Rseq . (m,j) by MESFUNC9:def 6;
hence (ProjMap1 (Rseq,m)) . j >= 0 by a1; :: thesis: verum
end;
then ProjMap1 (Rseq,m) is nonnegative-yielding ;
then (ProjMap1 (Rseq,m)) . n <= (Partial_Sums (ProjMap1 (Rseq,m))) . n by th101;
then (ProjMap1 (Rseq,m)) . n <= (Partial_Sums_in_cod2 Rseq) . (m,n) by th100;
hence Rseq . (m1,n1) <= (Partial_Sums_in_cod2 Rseq) . (m1,n1) by MESFUNC9:def 6; :: thesis: verum
end;