let G be RealNormSpace-Sequence; :: thesis: for seq being sequence of (product G)

for x0 being Point of (product G)

for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds

for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let seq be sequence of (product G); :: thesis: for x0 being Point of (product G)

for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds

for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let x0 be Point of (product G); :: thesis: for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds

for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let y0 be Element of product (carr G); :: thesis: ( x0 = y0 & seq is convergent & lim seq = x0 implies for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) )

assume that

A1: x0 = y0 and

A2: ( seq is convergent & lim seq = x0 ) ; :: thesis: for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let i be Element of dom G; :: thesis: ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

defpred S_{1}[ Nat, Element of (G . i)] means ex seqm being Element of product (carr G) st

( seqm = seq . $1 & $2 = seqm . i );

len G = len (carr G) by Def4;

then A3: dom G = dom (carr G) by FINSEQ_3:29;

then y0 . i in (carr G) . i by CARD_3:9;

then reconsider x0i = y0 . i as Point of (G . i) by Def4;

A4: for x being Element of NAT ex y being Element of (G . i) st S_{1}[x,y]

A6: for x being Element of NAT holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A4);

for x being Nat holds S_{1}[x,f . x]

A7: for m being Nat ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ;

take seqi ; :: thesis: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

A8: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((seqi . n) - x0i).|| < r

hence ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) by A7, A8, NORMSP_1:def 7; :: thesis: verum

for x0 being Point of (product G)

for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds

for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let seq be sequence of (product G); :: thesis: for x0 being Point of (product G)

for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds

for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let x0 be Point of (product G); :: thesis: for y0 being Element of product (carr G) st x0 = y0 & seq is convergent & lim seq = x0 holds

for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let y0 be Element of product (carr G); :: thesis: ( x0 = y0 & seq is convergent & lim seq = x0 implies for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) )

assume that

A1: x0 = y0 and

A2: ( seq is convergent & lim seq = x0 ) ; :: thesis: for i being Element of dom G ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

let i be Element of dom G; :: thesis: ex seqi being sequence of (G . i) st

( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

defpred S

( seqm = seq . $1 & $2 = seqm . i );

len G = len (carr G) by Def4;

then A3: dom G = dom (carr G) by FINSEQ_3:29;

then y0 . i in (carr G) . i by CARD_3:9;

then reconsider x0i = y0 . i as Point of (G . i) by Def4;

A4: for x being Element of NAT ex y being Element of (G . i) st S

proof

consider f being sequence of the carrier of (G . i) such that
let x be Element of NAT ; :: thesis: ex y being Element of (G . i) st S_{1}[x,y]

product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

then consider seqm being Element of product (carr G) such that

A5: seqm = seq . x ;

take seqm . i ; :: thesis: ( seqm . i is Element of (G . i) & S_{1}[x,seqm . i] )

(carr G) . i = the carrier of (G . i) by Def4;

hence ( seqm . i is Element of (G . i) & S_{1}[x,seqm . i] )
by A3, A5, CARD_3:9; :: thesis: verum

end;product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

then consider seqm being Element of product (carr G) such that

A5: seqm = seq . x ;

take seqm . i ; :: thesis: ( seqm . i is Element of (G . i) & S

(carr G) . i = the carrier of (G . i) by Def4;

hence ( seqm . i is Element of (G . i) & S

A6: for x being Element of NAT holds S

for x being Nat holds S

proof

then consider seqi being sequence of (G . i) such that
let x be Nat; :: thesis: S_{1}[x,f . x]

x in NAT by ORDINAL1:def 12;

hence S_{1}[x,f . x]
by A6; :: thesis: verum

end;x in NAT by ORDINAL1:def 12;

hence S

A7: for m being Nat ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ;

take seqi ; :: thesis: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) )

A8: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((seqi . n) - x0i).|| < r

proof

then
seqi is convergent
;
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for n being Nat st m <= n holds

||.((seqi . n) - x0i).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((seqi . n) - x0i).|| < r

then consider k being Nat such that

A9: for n being Nat st k <= n holds

||.((seq . n) - x0).|| < r by A2, NORMSP_1:def 7;

take k ; :: thesis: for n being Nat st k <= n holds

||.((seqi . n) - x0i).|| < r

let n be Nat; :: thesis: ( k <= n implies ||.((seqi . n) - x0i).|| < r )

assume n >= k ; :: thesis: ||.((seqi . n) - x0i).|| < r

then A10: ||.((seq . n) - x0).|| < r by A9;

ex seqn being Element of product (carr G) st

( seqn = seq . n & seqi . n = seqn . i ) by A7;

then ||.((seqi . n) - x0i).|| <= ||.((seq . n) - x0).|| by A1, Th11;

hence ||.((seqi . n) - x0i).|| < r by A10, XXREAL_0:2; :: thesis: verum

end;for n being Nat st m <= n holds

||.((seqi . n) - x0i).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((seqi . n) - x0i).|| < r

then consider k being Nat such that

A9: for n being Nat st k <= n holds

||.((seq . n) - x0).|| < r by A2, NORMSP_1:def 7;

take k ; :: thesis: for n being Nat st k <= n holds

||.((seqi . n) - x0i).|| < r

let n be Nat; :: thesis: ( k <= n implies ||.((seqi . n) - x0i).|| < r )

assume n >= k ; :: thesis: ||.((seqi . n) - x0i).|| < r

then A10: ||.((seq . n) - x0).|| < r by A9;

ex seqn being Element of product (carr G) st

( seqn = seq . n & seqi . n = seqn . i ) by A7;

then ||.((seqi . n) - x0i).|| <= ||.((seq . n) - x0).|| by A1, Th11;

hence ||.((seqi . n) - x0i).|| < r by A10, XXREAL_0:2; :: thesis: verum

hence ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . i ) ) ) by A7, A8, NORMSP_1:def 7; :: thesis: verum