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];

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 )

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

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

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 A18:
( <:seqx,seqy:> is convergent & lim <:seqx,seqy:> = [x,y] )
; :: thesis: ( 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

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

end;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

hence
<:seqx,seqy:> is convergent
; :: thesis: lim <:seqx,seqy:> = [x,y]
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;

hence ||.((<:seqx,seqy:> . n) - [x,y]).|| < r1 by A13, A4, XXREAL_0:2; :: thesis: verum

end;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

then
|.w.| <= 2 * ((r1 / 2) / 2)
by PDIFF_8:17;|.((proj (i,2)) . w).| <= (r1 / 2) / 2

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= 2 implies |.((proj (b_{1},2)) . w).| <= (r1 / 2) / 2 )

assume ( 1 <= i & i <= 2 ) ; :: thesis: |.((proj (b_{1},2)) . w).| <= (r1 / 2) / 2

then A14: i in Seg 2 by FINSEQ_1:1;

end;assume ( 1 <= i & i <= 2 ) ; :: thesis: |.((proj (b

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;

end;

suppose A15:
i = 1
; :: thesis: |.((proj (b_{1},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;.= ||.((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

suppose
i = 2
; :: thesis: |.((proj (b_{1},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;.= ||.((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

hence ||.((<:seqx,seqy:> . n) - [x,y]).|| < r1 by A13, A4, XXREAL_0:2; :: thesis: verum

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

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

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

hence
seqx is convergent
; :: thesis: ( lim seqx = x & seqy is convergent & lim seqy = y )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;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

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

hence
seqy is convergent
; :: thesis: lim seqy = yex 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;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

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