let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding & Partial_Sums Rseq is P-convergent implies ( Partial_Sums_in_cod1 Rseq is convergent_in_cod1 & Partial_Sums_in_cod2 Rseq is convergent_in_cod2 ) )
assume that
A1: Rseq is nonnegative-yielding and
A2: Partial_Sums Rseq is P-convergent ; :: thesis: ( Partial_Sums_in_cod1 Rseq is convergent_in_cod1 & Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )

now :: thesis: for k being Element of NAT holds ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is convergent

let k be Element of NAT ; :: thesis: ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is convergent
B1: ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is non-decreasing by A1, th1005;

now :: thesis: for n being Nat holds (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n < (P-lim (Partial_Sums Rseq)) + 2

let n be Nat; :: thesis: (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n < (P-lim (Partial_Sums Rseq)) + 2
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
B2: (Partial_Sums Rseq) . (n,k) = (Partial_Sums (ProjMap1 ((Partial_Sums_in_cod1 Rseq),n1))) . k by th100;
B3: (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n1 = (Partial_Sums_in_cod1 Rseq) . (n1,k) by MESFUNC9:def 7
.= (ProjMap1 ((Partial_Sums_in_cod1 Rseq),n1)) . k by MESFUNC9:def 6 ;

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

let d be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod1 Rseq),n1)) . d >= 0
ProjMap1 ((Partial_Sums_in_cod1 Rseq),n1) is nonnegative by A1, th1005;
hence (ProjMap1 ((Partial_Sums_in_cod1 Rseq),n1)) . d >= 0 ; :: thesis: verum

end;

then ProjMap1 ((Partial_Sums_in_cod1 Rseq),n1) is nonnegative-yielding ;
then B4: (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n1 <= (Partial_Sums Rseq) . (n,k) by B2, B3, th101;
consider N being Nat such that
B6: for n, m being Nat st n >= N & m >= N holds
|.(((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq))).| < 1 by A2, DBLSEQ_1:def 2;
reconsider N1 = max (N,(max (k,n))) as Nat by TARSKI:1;
B7: ( N1 >= N & N1 >= max (k,n) & max (k,n) >= k & max (k,n) >= n ) by XXREAL_0:25;
then |.(((Partial_Sums Rseq) . (N1,N1)) - (P-lim (Partial_Sums Rseq))).| < 1 by B6;
then ((Partial_Sums Rseq) . (N1,N1)) - (P-lim (Partial_Sums Rseq)) <= 1 by ABSVALUE:5;
then ((Partial_Sums Rseq) . (N1,N1)) - (P-lim (Partial_Sums Rseq)) < 2 by XXREAL_0:2;
then B8: (Partial_Sums Rseq) . (N1,N1) < (P-lim (Partial_Sums Rseq)) + 2 by XREAL_1:19;
B9: ( N1 >= k & N1 >= n ) by B7, XXREAL_0:2;
Partial_Sums Rseq is non-decreasing by A1, th80a;
then (Partial_Sums Rseq) . (n,k) <= (Partial_Sums Rseq) . (N1,N1) by B9;
then (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n <= (Partial_Sums Rseq) . (N1,N1) by B4, XXREAL_0:2;
hence (ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n < (P-lim (Partial_Sums Rseq)) + 2 by B8, XXREAL_0:2; :: thesis: verum

end;

then ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is bounded_above by SEQ_2:def 3;
hence ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is convergent by B1; :: thesis: verum

end;

hence Partial_Sums_in_cod1 Rseq is convergent_in_cod1 ; :: thesis: Partial_Sums_in_cod2 Rseq is convergent_in_cod2

now :: thesis: for k being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent

let k be Element of NAT ; :: thesis: ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent
C1: ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is non-decreasing by A1, th1005;

now :: thesis: for n being Nat holds (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n < (P-lim (Partial_Sums Rseq)) + 2

let n be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n < (P-lim (Partial_Sums Rseq)) + 2
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
B2: (Partial_Sums Rseq) . (k,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (k,n) by th103
.= (Partial_Sums (ProjMap2 ((Partial_Sums_in_cod2 Rseq),n1))) . k by th100 ;
B3: (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n1 = (Partial_Sums_in_cod2 Rseq) . (k,n1) by MESFUNC9:def 6
.= (ProjMap2 ((Partial_Sums_in_cod2 Rseq),n1)) . k by MESFUNC9:def 7 ;

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

let d be Nat; :: thesis: (ProjMap2 ((Partial_Sums_in_cod2 Rseq),n1)) . d >= 0
ProjMap2 ((Partial_Sums_in_cod2 Rseq),n1) is nonnegative by A1, th1005;
hence (ProjMap2 ((Partial_Sums_in_cod2 Rseq),n1)) . d >= 0 ; :: thesis: verum

end;

then ProjMap2 ((Partial_Sums_in_cod2 Rseq),n1) is nonnegative-yielding ;
then B4: (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n1 <= (Partial_Sums Rseq) . (k,n) by B2, B3, th101;
consider N being Nat such that
B6: for n, m being Nat st n >= N & m >= N holds
|.(((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq))).| < 1 by A2, DBLSEQ_1:def 2;
reconsider N1 = max (N,(max (k,n))) as Nat by TARSKI:1;
B7: ( N1 >= N & N1 >= max (k,n) & max (k,n) >= k & max (k,n) >= n ) by XXREAL_0:25;
then |.(((Partial_Sums Rseq) . (N1,N1)) - (P-lim (Partial_Sums Rseq))).| < 1 by B6;
then ((Partial_Sums Rseq) . (N1,N1)) - (P-lim (Partial_Sums Rseq)) <= 1 by ABSVALUE:5;
then ((Partial_Sums Rseq) . (N1,N1)) - (P-lim (Partial_Sums Rseq)) < 2 by XXREAL_0:2;
then B8: (Partial_Sums Rseq) . (N1,N1) < (P-lim (Partial_Sums Rseq)) + 2 by XREAL_1:19;
B9: ( N1 >= k & N1 >= n ) by B7, XXREAL_0:2;
Partial_Sums Rseq is non-decreasing by A1, th80a;
then (Partial_Sums Rseq) . (k,n) <= (Partial_Sums Rseq) . (N1,N1) by B9;
then (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n <= (Partial_Sums Rseq) . (N1,N1) by B4, XXREAL_0:2;
hence (ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n < (P-lim (Partial_Sums Rseq)) + 2 by B8, XXREAL_0:2; :: thesis: verum

end;

then ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is bounded_above by SEQ_2:def 3;
hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent by C1; :: thesis: verum

end;

hence Partial_Sums_in_cod2 Rseq is convergent_in_cod2 ; :: thesis: verum