let X be non empty set ; :: thesis: for Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedFunctions X,Y) st seq is CCauchy holds
seq is convergent
let Y be RealNormSpace; :: thesis: ( Y is complete implies for seq being sequence of (R_NormSpace_of_BoundedFunctions X,Y) st seq is CCauchy holds
seq is convergent )
assume A1:
Y is complete
; :: thesis: for seq being sequence of (R_NormSpace_of_BoundedFunctions X,Y) st seq is CCauchy holds
seq is convergent
let vseq be sequence of (R_NormSpace_of_BoundedFunctions X,Y); :: thesis: ( vseq is CCauchy implies vseq is convergent )
assume A2:
vseq is CCauchy
; :: thesis: vseq is convergent
A3:
||.vseq.|| is convergent
defpred S1[ set , set ] means ex xseq being sequence of Y st
( ( for n being Element of NAT holds xseq . n = (modetrans (vseq . n),X,Y) . $1 ) & xseq is convergent & $2 = lim xseq );
A11:
for x being Element of X ex y being Element of Y st S1[x,y]
proof
let x be
Element of
X;
:: thesis: ex y being Element of Y st S1[x,y]
deffunc H1(
Element of
NAT )
-> Element of the
carrier of
Y =
(modetrans (vseq . $1),X,Y) . x;
consider xseq being
sequence of
Y such that A12:
for
n being
Element of
NAT holds
xseq . n = H1(
n)
from FUNCT_2:sch 4();
A13:
for
m,
k being
Element of
NAT holds
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
proof
let m,
k be
Element of
NAT ;
:: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
vseq . m is
bounded Function of
X,the
carrier of
Y
by Def5;
then A14:
modetrans (vseq . m),
X,
Y = vseq . m
by Th16;
vseq . k is
bounded Function of
X,the
carrier of
Y
by Def5;
then A15:
modetrans (vseq . k),
X,
Y = vseq . k
by Th16;
reconsider h1 =
(vseq . m) - (vseq . k) as
bounded Function of
X,the
carrier of
Y by Def5;
A16:
xseq . m = (modetrans (vseq . m),X,Y) . x
by A12;
xseq . k = (modetrans (vseq . k),X,Y) . x
by A12;
then
(xseq . m) - (xseq . k) = h1 . x
by A14, A15, A16, Th27;
hence
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
by Th19;
:: thesis: verum
end;
A17:
xseq is
convergent
take y =
lim xseq;
:: thesis: S1[x,y]
thus
S1[
x,
y]
by A12, A17;
:: thesis: verum
end;
consider f being Function of X,the carrier of Y such that
A22:
for x being Element of X holds S1[x,f . x]
from FUNCT_2:sch 3(A11);
reconsider tseq = f as Function of X,the carrier of Y ;
A23:
tseq is bounded
A31:
for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e
proof
let e be
Real;
:: thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e )
assume A32:
e > 0
;
:: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e
consider k being
Element of
NAT such that A33:
for
n,
m being
Element of
NAT st
n >= k &
m >= k holds
||.((vseq . n) - (vseq . m)).|| < e
by A2, A32, RSSPACE3:10;
A34:
now let n be
Element of
NAT ;
:: thesis: ( n >= k implies for x being Element of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e )assume A35:
n >= k
;
:: thesis: for x being Element of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= enow let x be
Element of
X;
:: thesis: ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= econsider xseq being
sequence of
Y such that A36:
( ( for
n being
Element of
NAT holds
xseq . n = (modetrans (vseq . n),X,Y) . x ) &
xseq is
convergent &
tseq . x = lim xseq )
by A22;
A37:
for
m,
k being
Element of
NAT holds
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
proof
let m,
k be
Element of
NAT ;
:: thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
vseq . m is
bounded Function of
X,the
carrier of
Y
by Def5;
then A38:
modetrans (vseq . m),
X,
Y = vseq . m
by Th16;
vseq . k is
bounded Function of
X,the
carrier of
Y
by Def5;
then A39:
modetrans (vseq . k),
X,
Y = vseq . k
by Th16;
reconsider h1 =
(vseq . m) - (vseq . k) as
bounded Function of
X,the
carrier of
Y by Def5;
A40:
xseq . m = (modetrans (vseq . m),X,Y) . x
by A36;
xseq . k = (modetrans (vseq . k),X,Y) . x
by A36;
then
(xseq . m) - (xseq . k) = h1 . x
by A38, A39, A40, Th27;
hence
||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).||
by Th19;
:: thesis: verum
end; A41:
for
m being
Element of
NAT st
m >= k holds
||.((xseq . n) - (xseq . m)).|| <= e
||.((xseq . n) - (tseq . x)).|| <= e
hence
||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e
by A36;
:: thesis: verum end; hence
for
x being
Element of
X holds
||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e
;
:: thesis: verum end;
take
k
;
:: thesis: for n being Element of NAT st n >= k holds
for x being Element of X holds ||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e
thus
for
n being
Element of
NAT st
n >= k holds
for
x being
Element of
X holds
||.(((modetrans (vseq . n),X,Y) . x) - (tseq . x)).|| <= e
by A34;
:: thesis: verum
end;
reconsider tseq = tseq as bounded Function of X,the carrier of Y by A23;
reconsider tv = tseq as Point of (R_NormSpace_of_BoundedFunctions X,Y) by Def5;
A50:
for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
hence
vseq is convergent
by NORMSP_1:def 9; :: thesis: verum