let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums Rseq is convergent_in_cod2 iff Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )
hereby :: thesis: ( Partial_Sums_in_cod2 Rseq is convergent_in_cod2 implies Partial_Sums Rseq is convergent_in_cod2 )
assume A1: Partial_Sums Rseq is convergent_in_cod2 ; :: thesis: Partial_Sums_in_cod2 Rseq is convergent_in_cod2
now :: thesis: for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 Rseq),m) is convergent
let m be Element of NAT ; :: thesis: ProjMap1 ((Partial_Sums_in_cod2 Rseq),m) is convergent
defpred S1[ Nat] means for k being Element of NAT st k = $1 holds
ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent ;
then A3: S1[ 0 ] ;
A4: for m1 being Nat st S1[m1] holds
S1[m1 + 1]
proof
let m1 be Nat; :: thesis: ( S1[m1] implies S1[m1 + 1] )
reconsider m = m1 as Element of NAT by ORDINAL1:def 12;
assume S1[m1] ; :: thesis: S1[m1 + 1]
hereby :: thesis: verum
let k be Element of NAT ; :: thesis: ( k = m1 + 1 implies ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent )
assume B2: k = m1 + 1 ; :: thesis: ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent
then reconsider k1 = k - 1 as Element of NAT by NAT_1:11, NAT_1:21;
B4: ( ProjMap1 ((Partial_Sums Rseq),m) is convergent & ProjMap1 ((Partial_Sums Rseq),k) is convergent ) by A1;
now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e )
assume B6: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e
then consider N1 being Nat such that
B7: for n being Nat st n >= N1 holds
|.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| < e / 2 by B4, SEQ_2:def 7;
consider N2 being Nat such that
B8: for n being Nat st n >= N2 holds
|.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| < e / 2 by B4, B6, SEQ_2:def 7;
reconsider N = max (N1,N2) as Nat by TARSKI:1;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e
hereby :: thesis: verum
let n be Nat; :: thesis: ( n >= N implies |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e )
assume B9: n >= N ; :: thesis: |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e
( N >= N1 & N >= N2 ) by XXREAL_0:25;
then ( n >= N1 & n >= N2 ) by B9, XXREAL_0:2;
then ( |.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| < e / 2 & |.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| < e / 2 ) by B7, B8;
then B12: |.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| + |.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| < (e / 2) + (e / 2) by XREAL_1:8;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
(ProjMap1 ((Partial_Sums Rseq),k)) . n = (Partial_Sums Rseq) . (k,n1) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((m + 1),n1) by B2, th103a
.= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,n1)) + ((Partial_Sums_in_cod2 Rseq) . ((m + 1),n1)) by DefRS
.= ((Partial_Sums Rseq) . (m,n1)) + ((Partial_Sums_in_cod2 Rseq) . (k,n1)) by B2, th103a
.= ((ProjMap1 ((Partial_Sums Rseq),m)) . n) + ((Partial_Sums_in_cod2 Rseq) . (k,n1)) by MESFUNC9:def 6
.= ((ProjMap1 ((Partial_Sums Rseq),m)) . n) + ((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) by MESFUNC9:def 6 ;
then |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| = |.((((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))) - (((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| ;
then |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| <= |.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| + |.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| by COMPLEX1:57;
hence |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e by B12, XXREAL_0:2; :: thesis: verum
end;
end;
hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent by SEQ_2:def 6; :: thesis: verum
end;
end;
for m1 being Nat holds S1[m1] from NAT_1:sch 2(A3, A4);
hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),m) is convergent ; :: thesis: verum
end;
hence Partial_Sums_in_cod2 Rseq is convergent_in_cod2 ; :: thesis: verum
end;
assume C0: Partial_Sums_in_cod2 Rseq is convergent_in_cod2 ; :: thesis: Partial_Sums Rseq is convergent_in_cod2
now :: thesis: for m being Element of NAT holds ProjMap1 ((Partial_Sums Rseq),m) is convergent
let m be Element of NAT ; :: thesis: ProjMap1 ((Partial_Sums Rseq),m) is convergent
defpred S1[ Nat] means for k being Element of NAT st k = $1 holds
ProjMap1 ((Partial_Sums Rseq),k) is convergent ;
ProjMap1 ((Partial_Sums Rseq),0) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),0) by th00;
then C1: S1[ 0 ] by C0;
C2: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume C3: S1[m] ; :: thesis: S1[m + 1]
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
hereby :: thesis: verum
let k be Element of NAT ; :: thesis: ( k = m + 1 implies ProjMap1 ((Partial_Sums Rseq),k) is convergent )
assume C4: k = m + 1 ; :: thesis: ProjMap1 ((Partial_Sums Rseq),k) is convergent
then reconsider k1 = k - 1 as Element of NAT by NAT_1:11, NAT_1:21;
for n being Element of NAT holds (ProjMap1 ((Partial_Sums Rseq),k)) . n = ((ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)))) . n
proof
let n be Element of NAT ; :: thesis: (ProjMap1 ((Partial_Sums Rseq),k)) . n = ((ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)))) . n
(ProjMap1 ((Partial_Sums Rseq),k)) . n = (Partial_Sums Rseq) . ((m1 + 1),n) by C4, MESFUNC9:def 6
.= ((Partial_Sums_in_cod2 Rseq) . ((m1 + 1),n)) + ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq)) . (m1,n)) by ThRS
.= ((ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1))) . n) + ((Partial_Sums Rseq) . (m1,n)) by MESFUNC9:def 6
.= ((ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1))) . n) + ((ProjMap1 ((Partial_Sums Rseq),m1)) . n) by MESFUNC9:def 6 ;
hence (ProjMap1 ((Partial_Sums Rseq),k)) . n = ((ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)))) . n by VALUED_1:1; :: thesis: verum
end;
then C5: ProjMap1 ((Partial_Sums Rseq),k) = (ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1))) ;
( ProjMap1 ((Partial_Sums Rseq),m1) is convergent & ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)) is convergent ) by C3, C0;
hence ProjMap1 ((Partial_Sums Rseq),k) is convergent by C5, SEQ_2:5; :: thesis: verum
end;
end;
for m being Nat holds S1[m] from NAT_1:sch 2(C1, C2);
hence ProjMap1 ((Partial_Sums Rseq),m) is convergent ; :: thesis: verum
end;
hence Partial_Sums Rseq is convergent_in_cod2 ; :: thesis: verum