let X, Y be RealNormSpace; :: thesis: for seqx being sequence of X
for seqy being sequence of Y
for x being Point of X
for y being Point of Y holds
( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y iff ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] ) )
let seqx be sequence of X; :: thesis: for seqy being sequence of Y
for x being Point of X
for y being Point of Y holds
( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y iff ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] ) )
let seqy be sequence of Y; :: thesis: for x being Point of X
for y being Point of Y holds
( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y iff ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] ) )
let x be Point of X; :: thesis: for y being Point of Y holds
( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y iff ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] ) )
let y be Point of Y; :: thesis: ( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y iff ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] ) )
set seq = <:seqx,seqy:>;
set v = [x,y];

hereby :: thesis: ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] implies ( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y ) )

assume A1: ( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y ) ; :: thesis: ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] )
A2: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((<:seqx,seqy:> . n) - [x,y]).|| < r

proof

let r1 be Real; :: thesis: ( 0 < r1 implies ex m being Nat st
for n being Nat st m <= n holds
||.((<:seqx,seqy:> . n) - [x,y]).|| < r1 )
assume A3: 0 < r1 ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((<:seqx,seqy:> . n) - [x,y]).|| < r1
set r = r1 / 2;
A4: ( 0 < r1 / 2 & r1 / 2 < r1 ) by A3, XREAL_1:215, XREAL_1:216;
set r2 = (r1 / 2) / 2;
A5: ( 0 < (r1 / 2) / 2 & (r1 / 2) / 2 < r1 / 2 ) by A4, XREAL_1:215, XREAL_1:216;
then consider m1 being Nat such that
A6: for n being Nat st m1 <= n holds
||.((seqx . n) - x).|| < (r1 / 2) / 2 by A1, NORMSP_1:def 7;
consider m2 being Nat such that
A7: for n being Nat st m2 <= n holds
||.((seqy . n) - y).|| < (r1 / 2) / 2 by A1, A5, NORMSP_1:def 7;
reconsider m = max (m1,m2) as Nat by TARSKI:1;
take m ; :: thesis: for n being Nat st m <= n holds
||.((<:seqx,seqy:> . n) - [x,y]).|| < r1
let n be Nat; :: thesis: ( m <= n implies ||.((<:seqx,seqy:> . n) - [x,y]).|| < r1 )
assume A8: m <= n ; :: thesis: ||.((<:seqx,seqy:> . n) - [x,y]).|| < r1
m1 <= m by XXREAL_0:25;
then A9: m1 <= n by A8, XXREAL_0:2;
m2 <= m by XXREAL_0:25;
then A10: m2 <= n by A8, XXREAL_0:2;
n in NAT by ORDINAL1:def 12;
then A11: [(seqx . n),(seqy . n)] = <:seqx,seqy:> . n by FUNCT_3:59;
A12: - [x,y] = [(- x),(- y)] by PRVECT_3:18;
(<:seqx,seqy:> . n) - [x,y] = [((seqx . n) - x),((seqy . n) - y)] by A11, A12, PRVECT_3:18;
then consider w being Element of REAL 2 such that
A13: ( w = <*||.((seqx . n) - x).||,||.((seqy . n) - y).||*> & ||.((<:seqx,seqy:> . n) - [x,y]).|| = |.w.| ) by PRVECT_3:18;

now :: thesis: for i being Element of NAT st 1 <= i & i <= 2 holds
|.((proj (i,2)) . w).| <= (r1 / 2) / 2

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= 2 implies |.((proj (b₁,2)) . w).| <= (r1 / 2) / 2 )
assume ( 1 <= i & i <= 2 ) ; :: thesis: |.((proj (b₁,2)) . w).| <= (r1 / 2) / 2
then A14: i in Seg 2 by FINSEQ_1:1;

per cases ( i = 1 or i = 2 ) by A14, FINSEQ_1:2, TARSKI:def 2;

suppose A15: i = 1 ; :: thesis: |.((proj (b₁,2)) . w).| <= (r1 / 2) / 2

A16: (proj (i,2)) . w = w . 1 by A15, PDIFF_1:def 1
.= ||.((seqx . n) - x).|| by A13, FINSEQ_1:44 ;
|.((proj (i,2)) . w).| = ||.((seqx . n) - x).|| by ABSVALUE:def 1, A16;
hence |.((proj (i,2)) . w).| <= (r1 / 2) / 2 by A9, A6; :: thesis: verum

end;

suppose i = 2 ; :: thesis: |.((proj (b₁,2)) . w).| <= (r1 / 2) / 2

then A17: (proj (i,2)) . w = w . 2 by PDIFF_1:def 1
.= ||.((seqy . n) - y).|| by A13, FINSEQ_1:44 ;
|.((proj (i,2)) . w).| = ||.((seqy . n) - y).|| by ABSVALUE:def 1, A17;
hence |.((proj (i,2)) . w).| <= (r1 / 2) / 2 by A10, A7; :: thesis: verum

end;

end;

end;

then |.w.| <= 2 * ((r1 / 2) / 2) by PDIFF_8:17;
hence ||.((<:seqx,seqy:> . n) - [x,y]).|| < r1 by A13, A4, XXREAL_0:2; :: thesis: verum

end;

hence <:seqx,seqy:> is convergent ; :: thesis: lim <:seqx,seqy:> = [x,y]
hence lim <:seqx,seqy:> = [x,y] by A2, NORMSP_1:def 7; :: thesis: verum

end;

assume A18: ( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] ) ; :: thesis: ( seqx is convergent & lim seqx = x & seqy is convergent & lim seqy = y )
A19: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r )

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r ) )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r )
then consider m being Nat such that
A20: for n being Nat st m <= n holds
||.((<:seqx,seqy:> . n) - [x,y]).|| < r by A18, NORMSP_1:def 7;
take m ; :: thesis: for n being Nat st m <= n holds
( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r )
let n be Nat; :: thesis: ( m <= n implies ( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r ) )
assume m <= n ; :: thesis: ( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r )
then A21: ||.((<:seqx,seqy:> . n) - [x,y]).|| < r by A20;
n in NAT by ORDINAL1:def 12;
then A22: [(seqx . n),(seqy . n)] = <:seqx,seqy:> . n by FUNCT_3:59;
A23: - [x,y] = [(- x),(- y)] by PRVECT_3:18;
(<:seqx,seqy:> . n) - [x,y] = [((seqx . n) - x),((seqy . n) - y)] by A22, A23, PRVECT_3:18;
then consider w being Element of REAL 2 such that
A24: ( w = <*||.((seqx . n) - x).||,||.((seqy . n) - y).||*> & ||.((<:seqx,seqy:> . n) - [x,y]).|| = |.w.| ) by PRVECT_3:18;
(proj (1,2)) . w = w . 1 by PDIFF_1:def 1
.= ||.((seqx . n) - x).|| by A24, FINSEQ_1:44 ;
then |.||.((seqx . n) - x).||.| <= |.w.| by PDIFF_8:5;
then ||.((seqx . n) - x).|| <= |.w.| by ABSVALUE:def 1;
hence ||.((seqx . n) - x).|| < r by A24, A21, XXREAL_0:2; :: thesis: ||.((seqy . n) - y).|| < r
(proj (2,2)) . w = w . 2 by PDIFF_1:def 1
.= ||.((seqy . n) - y).|| by A24, FINSEQ_1:44 ;
then |.||.((seqy . n) - y).||.| <= |.w.| by PDIFF_8:5;
then ||.((seqy . n) - y).|| <= |.w.| by ABSVALUE:def 1;
hence ||.((seqy . n) - y).|| < r by A24, A21, XXREAL_0:2; :: thesis: verum

end;

A25: now :: thesis: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seqx . n) - x).|| < r

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((seqx . n) - x).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((seqx . n) - x).|| < r
then consider m being Nat such that
A26: for n being Nat st m <= n holds
( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r ) by A19;
take m = m; :: thesis: for n being Nat st m <= n holds
||.((seqx . n) - x).|| < r
thus for n being Nat st m <= n holds
||.((seqx . n) - x).|| < r by A26; :: thesis: verum

end;

hence seqx is convergent ; :: thesis: ( lim seqx = x & seqy is convergent & lim seqy = y )
hence lim seqx = x by A25, NORMSP_1:def 7; :: thesis: ( seqy is convergent & lim seqy = y )

A27: now :: thesis: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seqy . n) - y).|| < r

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((seqy . n) - y).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((seqy . n) - y).|| < r
then consider m being Nat such that
A28: for n being Nat st m <= n holds
( ||.((seqx . n) - x).|| < r & ||.((seqy . n) - y).|| < r ) by A19;
take m = m; :: thesis: for n being Nat st m <= n holds
||.((seqy . n) - y).|| < r
thus for n being Nat st m <= n holds
||.((seqy . n) - y).|| < r by A28; :: thesis: verum

end;

hence seqy is convergent ; :: thesis: lim seqy = y
hence lim seqy = y by A27, NORMSP_1:def 7; :: thesis: verum