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₁[ Element of 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:31;
then y0 . i in (carr G) . i by CARD_3:18;
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₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of (G . i) st S₁[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 y = seqm . i; :: thesis: ( y is Element of (G . i) & S₁[x,y] )
(carr G) . i = the carrier of (G . i) by Def4;
hence ( y is Element of (G . i) & S₁[x,y] ) by A3, A5, CARD_3:18; :: thesis: verum

end;

ex f being Function of NAT ,the carrier of (G . i) st
for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A4);
then consider seqi being sequence of (G . i) such that
A6: for m being Element of 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 ) ) )
A7: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seqi . n) - x0i).|| < r

proof

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
||.((seqi . n) - x0i).|| < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seqi . n) - x0i).|| < r
then consider k being Element of NAT such that
A8: for n being Element of NAT st k <= n holds
||.((seq . n) - x0).|| < r by A2, NORMSP_1:def 11;

now

let n be Element of NAT ; :: thesis: ( n >= k implies ||.((seqi . n) - x0i).|| < r )
assume n >= k ; :: thesis: ||.((seqi . n) - x0i).|| < r
then A9: ||.((seq . n) - x0).|| < r by A8;
ex seqn being Element of product (carr G) st
( seqn = seq . n & seqi . n = seqn . i ) by A6;
then ||.((seqi . n) - x0i).|| <= ||.((seq . n) - x0).|| by A1, Th11;
hence ||.((seqi . n) - x0i).|| < r by A9, XXREAL_0:2; :: thesis: verum

end;

hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seqi . n) - x0i).|| < r ; :: thesis: verum

end;

then seqi is convergent by NORMSP_1:def 9;
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 A6, A7, NORMSP_1:def 11; :: thesis: verum