let X be non empty set ; for seq being sequence of (C_Normed_Algebra_of_BoundedFunctions X) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (C_Normed_Algebra_of_BoundedFunctions X); ( vseq is CCauchy implies vseq is convergent )
defpred S1[ set , set ] means ex xseq being Complex_Sequence st
for n being Nat holds
( xseq . n = (modetrans ((vseq . n),X)) . $1 & xseq is convergent & $2 = lim xseq );
assume A1:
vseq is CCauchy
; vseq is convergent
A2:
for x being Element of X ex y being Element of COMPLEX st S1[x,y]
proof
let x be
Element of
X;
ex y being Element of COMPLEX st S1[x,y]
deffunc H1(
Nat)
-> Element of
COMPLEX =
(modetrans ((vseq . $1),X)) . x;
consider xseq being
Complex_Sequence such that A3:
for
n being
Element of
NAT holds
xseq . n = H1(
n)
from FUNCT_2:sch 4();
A4:
for
n being
Nat holds
xseq . n = H1(
n)
reconsider y =
lim xseq as
Element of
COMPLEX by XCMPLX_0:def 2;
take
y
;
S1[x,y]
A5:
for
m,
k being
Nat holds
|.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
proof
let m,
k be
Nat;
|.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
A6:
(
m in NAT &
k in NAT )
by ORDINAL1:def 12;
(vseq . m) - (vseq . k) in ComplexBoundedFunctions X
;
then consider h1 being
Function of
X,
COMPLEX such that A7:
h1 = (vseq . m) - (vseq . k)
and A8:
h1 | X is
bounded
;
vseq . m in ComplexBoundedFunctions X
;
then
ex
vseqm being
Function of
X,
COMPLEX st
(
vseq . m = vseqm &
vseqm | X is
bounded )
;
then A9:
modetrans (
(vseq . m),
X)
= vseq . m
by Th12;
vseq . k in ComplexBoundedFunctions X
;
then
ex
vseqk being
Function of
X,
COMPLEX st
(
vseq . k = vseqk &
vseqk | X is
bounded )
;
then A10:
modetrans (
(vseq . k),
X)
= vseq . k
by Th12;
(
xseq . m = (modetrans ((vseq . m),X)) . x &
xseq . k = (modetrans ((vseq . k),X)) . x )
by A3, A6;
then
(xseq . m) - (xseq . k) = h1 . x
by A9, A10, A7, Th26;
hence
|.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
by A7, A8, Th19;
verum
end;
now for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < elet e be
Real;
( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e )assume
e > 0
;
ex k being Nat st
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < ethen consider k being
Nat such that A11:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A1, CSSPACE3:8;
reconsider k =
k as
Nat ;
take k =
k;
for n being Nat st n >= k holds
|.((xseq . n) - (xseq . k)).| < e end;
then
xseq is
convergent
by COMSEQ_3:46;
hence
S1[
x,
y]
by A4;
verum
end;
consider tseq being Function of X,COMPLEX such that
A13:
for x being Element of X holds S1[x,tseq . x]
from FUNCT_2:sch 3(A2);
then A18:
||.vseq.|| is convergent
by SEQ_4:41;
then
for x being Element of X st x in X /\ (dom tseq) holds
|.(tseq /. x).| <= lim ||.vseq.||
;
then
tseq | X is bounded
by CFUNCT_1:69;
then
tseq in ComplexBoundedFunctions X
;
then reconsider tv = tseq as Point of (C_Normed_Algebra_of_BoundedFunctions X) ;
A25:
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
proof
let e be
Real;
( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )
assume
e > 0
;
ex k being Nat st
for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
then consider k being
Nat such that A26:
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A1, CSSPACE3:8;
take
k
;
for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
now for n being Nat st n >= k holds
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= elet n be
Nat;
( n >= k implies for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e )assume A27:
n >= k
;
for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= enow for x being Element of X holds |.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= elet x be
Element of
X;
|.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= econsider xseq being
Complex_Sequence such that A28:
for
n being
Nat holds
xseq . n = (modetrans ((vseq . n),X)) . x
and A29:
xseq is
convergent
and A30:
tseq . x = lim xseq
by A13;
reconsider xn =
xseq . n as
Element of
COMPLEX by XCMPLX_0:def 2;
reconsider fseq =
NAT --> xn as
Complex_Sequence ;
set wseq =
xseq - fseq;
deffunc H1(
Nat)
-> object =
|.((xseq . $1) - (xseq . n)).|;
consider rseq being
Real_Sequence such that A31:
for
m being
Nat holds
rseq . m = H1(
m)
from SEQ_1:sch 1();
A32:
for
m,
k being
Nat holds
|.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
proof
let m,
k be
Nat;
|.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
(vseq . m) - (vseq . k) in ComplexBoundedFunctions X
;
then consider h1 being
Function of
X,
COMPLEX such that A33:
h1 = (vseq . m) - (vseq . k)
and A34:
h1 | X is
bounded
;
vseq . m in ComplexBoundedFunctions X
;
then
ex
vseqm being
Function of
X,
COMPLEX st
(
vseq . m = vseqm &
vseqm | X is
bounded )
;
then A35:
modetrans (
(vseq . m),
X)
= vseq . m
by Th12;
vseq . k in ComplexBoundedFunctions X
;
then
ex
vseqk being
Function of
X,
COMPLEX st
(
vseq . k = vseqk &
vseqk | X is
bounded )
;
then A36:
modetrans (
(vseq . k),
X)
= vseq . k
by Th12;
(
xseq . m = (modetrans ((vseq . m),X)) . x &
xseq . k = (modetrans ((vseq . k),X)) . x )
by A28;
then
(xseq . m) - (xseq . k) = h1 . x
by A35, A36, A33, Th26;
hence
|.((xseq . m) - (xseq . k)).| <= ||.((vseq . m) - (vseq . k)).||
by A33, A34, Th19;
verum
end; A37:
for
m being
Nat st
m >= k holds
rseq . m <= e
then A40:
rseq = |.(xseq - fseq).|
by FUNCT_2:12;
A41:
fseq is
convergent
by CFCONT_1:26;
A42:
lim rseq <= e
by A41, A37, A40, A29, RSSPACE2:5;
lim fseq = fseq . 0
by CFCONT_1:28;
then
lim fseq = xseq . n
;
then
lim (xseq - fseq) = (tseq . x) - (xseq . n)
by A29, A30, A41, COMSEQ_2:26;
then
lim rseq = |.((tseq . x) - (xseq . n)).|
by A41, A29, A40, SEQ_2:27;
then
|.((xseq . n) - (tseq . x)).| <= e
by A42, COMPLEX1:60;
hence
|.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
by A28;
verum end; hence
for
x being
Element of
X holds
|.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
;
verum end;
hence
for
n being
Nat st
n >= k holds
for
x being
Element of
X holds
|.(((modetrans ((vseq . n),X)) . x) - (tseq . x)).| <= e
;
verum
end;
A43:
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| <= e
for e being Real st e > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
hence
vseq is convergent
; verum