A1:
dom <*X,Y*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
then A2:
product <*X,Y*> is complete
by PRVECT_2:14;
consider I being Function of [:X,Y:],(product <*X,Y*>) such that
A3:
( I is one-to-one & I is onto & ( for x being Point of X
for y being Point of Y holds I . (x,y) = <*x,y*> ) & ( for v, w being Point of [:X,Y:] holds I . (v + w) = (I . v) + (I . w) ) & ( for v being Point of [:X,Y:]
for r being Real holds I . (r * v) = r * (I . v) ) & 0. (product <*X,Y*>) = I . (0. [:X,Y:]) & ( for v being Point of [:X,Y:] holds ||.(I . v).|| = ||.v.|| ) )
by Th15;
now for seq being sequence of [:X,Y:] st seq is Cauchy_sequence_by_Norm holds
seq is convergent let seq be
sequence of
[:X,Y:];
( seq is Cauchy_sequence_by_Norm implies seq is convergent )assume A6:
seq is
Cauchy_sequence_by_Norm
;
seq is convergent reconsider Iseq =
I * seq as
sequence of
(product <*X,Y*>) ;
then
Iseq is
Cauchy_sequence_by_Norm
by RSSPACE3:8;
then A10:
Iseq is
convergent
by A2, LOPBAN_1:def 15;
(
dom (I ") = rng I &
rng (I ") = dom I )
by A3, FUNCT_1:33;
then
(
dom (I ") = the
carrier of
(product <*X,Y*>) &
rng (I ") = the
carrier of
[:X,Y:] )
by A3, FUNCT_2:def 1, FUNCT_2:def 3;
then reconsider Lseq =
(I ") . (lim Iseq) as
Point of
[:X,Y:] by FUNCT_1:3;
rng I = the
carrier of
(product <*X,Y*>)
by A3, FUNCT_2:def 3;
then A11:
I . Lseq = lim Iseq
by A3, FUNCT_1:35;
hence
seq is
convergent
by NORMSP_1:def 6;
verum end;
hence
[:X,Y:] is complete
by LOPBAN_1:def 15; verum