let Rseq be Function of [:NAT,NAT:],REAL; ( Partial_Sums Rseq is convergent_in_cod2 iff Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )
hereby ( 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
;
Partial_Sums_in_cod2 Rseq is convergent_in_cod2 now for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 Rseq),m) is convergent let m be
Element of
NAT ;
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;
( S1[m1] implies S1[m1 + 1] )
reconsider m =
m1 as
Element of
NAT by ORDINAL1:def 12;
assume
S1[
m1]
;
S1[m1 + 1]
hereby verum
let k be
Element of
NAT ;
( k = m1 + 1 implies ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent )assume B2:
k = m1 + 1
;
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 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))))).| < elet e be
Real;
( 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
;
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))))).| < ethen 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;
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))))).| < ehereby verum
let n be
Nat;
( 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
;
|.(((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;
verum
end; end; hence
ProjMap1 (
(Partial_Sums_in_cod2 Rseq),
k) is
convergent
by SEQ_2:def 6;
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
;
verum end; hence
Partial_Sums_in_cod2 Rseq is
convergent_in_cod2
;
verum
end;
assume C0:
Partial_Sums_in_cod2 Rseq is convergent_in_cod2
; Partial_Sums Rseq is convergent_in_cod2
now for m being Element of NAT holds ProjMap1 ((Partial_Sums Rseq),m) is convergent let m be
Element of
NAT ;
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;
( S1[m] implies S1[m + 1] )
assume C3:
S1[
m]
;
S1[m + 1]
reconsider m1 =
m as
Element of
NAT by ORDINAL1:def 12;
hereby verum
let k be
Element of
NAT ;
( k = m + 1 implies ProjMap1 ((Partial_Sums Rseq),k) is convergent )assume C4:
k = m + 1
;
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 ;
(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;
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;
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
;
verum end;
hence
Partial_Sums Rseq is convergent_in_cod2
; verum