A1: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;

now

let i be Element of dom <*X,Y*>; :: thesis: <*X,Y*> . i is complete
( i = 1 or i = 2 ) by A1, TARSKI:def 2;
hence <*X,Y*> . i is complete by FINSEQ_1:44; :: thesis: verum

end;

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 Element of 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;

A4: now

let v, w be Point of [:X,Y:]; :: thesis: I . (v - w) = (I . v) - (I . w)
thus I . (v - w) = I . (v + ((- 1) * w)) by RLVECT_1:16
.= (I . v) + (I . ((- 1) * w)) by A3
.= (I . v) + ((- 1) * (I . w)) by A3
.= (I . v) - (I . w) by RLVECT_1:16 ; :: thesis: verum

end;

A5: now

let v, w be Point of [:X,Y:]; :: thesis: ||.((I . v) - (I . w)).|| = ||.(v - w).||
thus ||.((I . v) - (I . w)).|| = ||.(I . (v - w)).|| by A4
.= ||.(v - w).|| by A3 ; :: thesis: verum

end;

now

let seq be sequence of [:X,Y:]; :: thesis: ( seq is CCauchy implies seq is convergent )
assume A6: seq is CCauchy ; :: thesis: seq is convergent
reconsider Iseq = I * seq as sequence of (product <*X,Y*>) ;

now

let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r
then consider k being Element of NAT such that
A7: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A6, RSSPACE3:8;
take k = k; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r

hereby :: thesis: verum

let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies ||.((Iseq . n) - (Iseq . m)).|| < r )
assume ( n >= k & m >= k ) ; :: thesis: ||.((Iseq . n) - (Iseq . m)).|| < r
then A8: ||.((seq . n) - (seq . m)).|| < r by A7;
NAT = dom seq by FUNCT_2:def 1;
then ( Iseq . n = I . (seq . n) & Iseq . m = I . (seq . m) ) by FUNCT_1:13;
hence ||.((Iseq . n) - (Iseq . m)).|| < r by A8, A5; :: thesis: verum

end;

end;

then Iseq is CCauchy by RSSPACE3:8;
then A9: 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 A10: I . Lseq = lim Iseq by A3, FUNCT_1:35;

now

let r be Real; :: thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r )
assume 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r
then consider m being Element of NAT such that
A11: for n being Element of NAT st m <= n holds
||.((Iseq . n) - (lim Iseq)).|| < r by A9, NORMSP_1:def 7;
take m = m; :: thesis: for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r
thus for n being Element of NAT st m <= n holds
||.((seq . n) - Lseq).|| < r :: thesis: verum

proof

let n be Element of NAT ; :: thesis: ( m <= n implies ||.((seq . n) - Lseq).|| < r )
assume m <= n ; :: thesis: ||.((seq . n) - Lseq).|| < r
then A12: ||.((Iseq . n) - (lim Iseq)).|| < r by A11;
NAT = dom seq by FUNCT_2:def 1;
then Iseq . n = I . (seq . n) by FUNCT_1:13;
hence ||.((seq . n) - Lseq).|| < r by A10, A5, A12; :: thesis: verum

end;

end;

hence seq is convergent by NORMSP_1:def 6; :: thesis: verum

end;

hence [:X,Y:] is complete by LOPBAN_1:def 15; :: thesis: verum