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₁[ 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 PRVECT_1:def 11;
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 PRVECT_1:def 11;
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 seqm . i ; :: thesis: ( seqm . i is Element of (G . i) & S₁[x,seqm . i] )
(carr G) . i = the carrier of (G . i) by PRVECT_1:def 11;
hence ( seqm . i is Element of (G . i) & S₁[x,seqm . i] ) by A3, A5, CARD_3:9; :: thesis: verum

end;

consider f being sequence of the carrier of (G . i) such that
A6: for x being Element of NAT holds S₁[x,f . x] from FUNCT_2:sch 3(A4);
for x being Nat holds S₁[x,f . x]

proof

let x be Nat; :: thesis: S₁[x,f . x]
x in NAT by ORDINAL1:def 12;
hence S₁[x,f . x] by A6; :: thesis: verum

end;

then consider seqi being sequence of (G . i) such that
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

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;

then seqi is convergent ;
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