A1: dom <*X,Y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
now :: thesis: for i being Element of dom <*X,Y*> holds <*X,Y*> . i is complete
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 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 :: thesis: for v, w being Point of [:X,Y:] holds I . (v - w) = (I . v) - (I . w)
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 :: thesis: for v, w being Point of [:X,Y:] holds ||.((I . v) - (I . w)).|| = ||.(v - w).||
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 :: thesis: 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:]; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume A6: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent
reconsider Iseq = I * seq as sequence of (product <*X,Y*>) ;
now :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r
then consider k being Nat such that
A7: for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A6, RSSPACE3:8;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((Iseq . n) - (Iseq . m)).|| < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((Iseq . n) - (Iseq . m)).|| < r )
A8: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
assume ( n >= k & m >= k ) ; :: thesis: ||.((Iseq . n) - (Iseq . m)).|| < r
then A9: ||.((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, A8;
hence ||.((Iseq . n) - (Iseq . m)).|| < r by A9, A5; :: thesis: verum
end;
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;
now :: thesis: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - Lseq).|| < r
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - Lseq).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - Lseq).|| < r
then consider m being Nat such that
A12: for n being Nat st m <= n holds
||.((Iseq . n) - (lim Iseq)).|| < r by A10, NORMSP_1:def 7;
take m = m; :: thesis: for n being Nat st m <= n holds
||.((seq . n) - Lseq).|| < r
let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - Lseq).|| < r )
A13: n in NAT by ORDINAL1:def 12;
assume m <= n ; :: thesis: ||.((seq . n) - Lseq).|| < r
then A14: ||.((Iseq . n) - (lim Iseq)).|| < r by A12;
NAT = dom seq by FUNCT_2:def 1;
then Iseq . n = I . (seq . n) by FUNCT_1:13, A13;
hence ||.((seq . n) - Lseq).|| < r by A11, A5, A14; :: thesis: verum
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