P3: dom <*X,Y*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;

now

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

end;

then P1: product <*X,Y*> is complete by PRVECT_2:14;
consider I being Function of [:X,Y:],(product <*X,Y*>) such that
P2: ( 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 ThHOM02;

H1: 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:29
.= (I . v) + (I . ((- 1) * w)) by P2
.= (I . v) + ((- 1) * (I . w)) by P2
.= (I . v) - (I . w) by RLVECT_1:29 ; :: thesis: verum

end;

H2: 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 H1
.= ||.(v - w).|| by P2 ; :: thesis: verum

end;

now

let seq be sequence of [:X,Y:]; :: thesis: ( seq is CCauchy implies seq is convergent )
assume P3: 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
P5: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by P3, RSSPACE3:10;
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 P6: ||.((seq . n) - (seq . m)).|| < r by P5;
NAT = dom seq by FUNCT_2:def 1;
then ( Iseq . n = I . (seq . n) & Iseq . m = I . (seq . m) ) by FUNCT_1:23;
hence ||.((Iseq . n) - (Iseq . m)).|| < r by P6, H2; :: thesis: verum

end;

end;

then Iseq is CCauchy by RSSPACE3:10;
then P7: Iseq is convergent by P1, LOPBAN_1:def 16;
( dom (I ") = rng I & rng (I ") = dom I ) by FUNCT_1:55, P2;
then ( dom (I ") = the carrier of (product <*X,Y*>) & rng (I ") = the carrier of [:X,Y:] ) by P2, FUNCT_2:def 1, FUNCT_2:def 3;
then reconsider Lseq = (I ") . (lim Iseq) as Point of [:X,Y:] by FUNCT_1:12;
rng I = the carrier of (product <*X,Y*>) by P2, FUNCT_2:def 3;
then P9: I . Lseq = lim Iseq by P2, FUNCT_1:57;

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
P10: for n being Element of NAT st m <= n holds
||.((Iseq . n) - (lim Iseq)).|| < r by P7, NORMSP_1:def 11;
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 P11: ||.((Iseq . n) - (lim Iseq)).|| < r by P10;
NAT = dom seq by FUNCT_2:def 1;
then Iseq . n = I . (seq . n) by FUNCT_1:23;
hence ||.((seq . n) - Lseq).|| < r by P9, H2, P11; :: thesis: verum

end;

end;

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

end;

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