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 & ( 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 ) ) ) ) holds

( seq is convergent & lim seq = x0 )

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 & ( 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 ) ) ) ) holds

( seq is convergent & lim seq = x0 )

let x0 be Point of (product G); :: thesis: for y0 being Element of product (carr G) st x0 = y0 & ( 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 ) ) ) ) holds

( seq is convergent & lim seq = x0 )

let y0 be Element of product (carr G); :: thesis: ( x0 = y0 & ( 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 ) ) ) ) implies ( seq is convergent & lim seq = x0 ) )

assume that

A1: x0 = y0 and

A2: 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 ) ) ) ; :: thesis: ( seq is convergent & lim seq = x0 )

defpred S_{1}[ Element of dom G, set ] means ex rseqi being Real_Sequence ex seqi being sequence of (G . $1) st

( rseqi = $2 & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . $1 ) ) );

A3: for i being Element of dom G ex yyseqi being Element of Funcs (NAT,REAL) st S_{1}[i,yyseqi]

A7: for i being Element of dom G holds S_{1}[i,yyseq . i]
from FUNCT_2:sch 3(A3);

reconsider I = len G as Element of NAT ;

defpred S_{2}[ Element of NAT , Element of REAL I] means for i being Element of dom G holds (yyseq . i) . $1 = $2 . i;

A8: for k being Element of NAT ex yseqk being Element of REAL I st S_{2}[k,yseqk]

A12: for k being Element of NAT holds S_{2}[k,yseq . k]
from FUNCT_2:sch 3(A8);

then reconsider xseq = yseq as sequence of (REAL-NS I) ;

xseq = yseq ;

then consider xseq being sequence of (REAL-NS I), yseq being sequence of (REAL I) such that

A15: xseq = yseq and

A16: for i0 being Element of NAT st i0 in Seg I holds

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

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 A13;

A17: for i being Nat st i in Seg I holds

ex rseqi being Real_Sequence st

( ( for k being Nat holds rseqi . k = (yseq . k) . i ) & rseqi is convergent & (0* I) . i = lim rseqi )

0* I = 0. (REAL-NS I) by REAL_NS1:def 4;

then ( xseq is convergent & lim xseq = 0. (REAL-NS I) ) by A15, A17, REAL_NS1:11;

then ( ||.(seq - x0).|| is convergent & lim ||.(seq - x0).|| = 0 ) by A35, Lm7;

hence ( seq is convergent & lim seq = x0 ) by Lm7; :: thesis: verum

for x0 being Point of (product G)

for y0 being Element of product (carr G) st x0 = y0 & ( 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 ) ) ) ) holds

( seq is convergent & lim seq = x0 )

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 & ( 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 ) ) ) ) holds

( seq is convergent & lim seq = x0 )

let x0 be Point of (product G); :: thesis: for y0 being Element of product (carr G) st x0 = y0 & ( 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 ) ) ) ) holds

( seq is convergent & lim seq = x0 )

let y0 be Element of product (carr G); :: thesis: ( x0 = y0 & ( 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 ) ) ) ) implies ( seq is convergent & lim seq = x0 ) )

assume that

A1: x0 = y0 and

A2: 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 ) ) ) ; :: thesis: ( seq is convergent & lim seq = x0 )

defpred S

( rseqi = $2 & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

( seqm = seq . m & seqi . m = seqm . $1 ) ) );

A3: for i being Element of dom G ex yyseqi being Element of Funcs (NAT,REAL) st S

proof

consider yyseq being Function of (dom G),(Funcs (NAT,REAL)) such that
let i be Element of dom G; :: thesis: ex yyseqi being Element of Funcs (NAT,REAL) st S_{1}[i,yyseqi]

consider seqi being sequence of (G . i) such that

A4: seqi is convergent and

y0 . i = lim seqi and

A5: for m being Element of NAT ex Sm being Element of product (carr G) st

( Sm = seq . m & seqi . m = Sm . i ) by A2;

set rseqi = ||.(seqi - (lim seqi)).||;

A6: ||.(seqi - (lim seqi)).|| is Element of Funcs (NAT,REAL) by FUNCT_2:8;

( ||.(seqi - (lim seqi)).|| is convergent & lim ||.(seqi - (lim seqi)).|| = 0 ) by A4, Lm7;

hence ex yyseqi being Element of Funcs (NAT,REAL) st S_{1}[i,yyseqi]
by A4, A5, A6; :: thesis: verum

end;consider seqi being sequence of (G . i) such that

A4: seqi is convergent and

y0 . i = lim seqi and

A5: for m being Element of NAT ex Sm being Element of product (carr G) st

( Sm = seq . m & seqi . m = Sm . i ) by A2;

set rseqi = ||.(seqi - (lim seqi)).||;

A6: ||.(seqi - (lim seqi)).|| is Element of Funcs (NAT,REAL) by FUNCT_2:8;

( ||.(seqi - (lim seqi)).|| is convergent & lim ||.(seqi - (lim seqi)).|| = 0 ) by A4, Lm7;

hence ex yyseqi being Element of Funcs (NAT,REAL) st S

A7: for i being Element of dom G holds S

reconsider I = len G as Element of NAT ;

defpred S

A8: for k being Element of NAT ex yseqk being Element of REAL I st S

proof

consider yseq being sequence of (REAL I) such that
let k be Element of NAT ; :: thesis: ex yseqk being Element of REAL I st S_{2}[k,yseqk]

defpred S_{3}[ set , object ] means ex i being Element of dom G st

( i = $1 & $2 = (yyseq . i) . k );

A9: for k being Nat st k in Seg I holds

ex x being object st S_{3}[k,x]

A10: ( dom yseqk = Seg I & ( for j being Nat st j in Seg I holds

S_{3}[j,yseqk . j] ) )
from FINSEQ_1:sch 1(A9);

yyy is Element of (len yyy) -tuples_on REAL by FINSEQ_2:92;

then reconsider yseqk = yseqk as Element of REAL I by A10, FINSEQ_1:def 3;

_{2}[k,yseqk]
; :: thesis: verum

end;defpred S

( i = $1 & $2 = (yyseq . i) . k );

A9: for k being Nat st k in Seg I holds

ex x being object st S

proof

consider yseqk being FinSequence such that
let j be Nat; :: thesis: ( j in Seg I implies ex x being object st S_{3}[j,x] )

assume j in Seg I ; :: thesis: ex x being object st S_{3}[j,x]

then reconsider i = j as Element of dom G by FINSEQ_1:def 3;

take (yyseq . i) . k ; :: thesis: S_{3}[j,(yyseq . i) . k]

thus S_{3}[j,(yyseq . i) . k]
; :: thesis: verum

end;assume j in Seg I ; :: thesis: ex x being object st S

then reconsider i = j as Element of dom G by FINSEQ_1:def 3;

take (yyseq . i) . k ; :: thesis: S

thus S

A10: ( dom yseqk = Seg I & ( for j being Nat st j in Seg I holds

S

now :: thesis: for j being Nat st j in dom yseqk holds

yseqk . j in REAL

then reconsider yyy = yseqk as FinSequence of REAL by FINSEQ_2:12;yseqk . j in REAL

let j be Nat; :: thesis: ( j in dom yseqk implies yseqk . j in REAL )

assume j in dom yseqk ; :: thesis: yseqk . j in REAL

then consider i being Element of dom G such that

i = j and

A11: yseqk . j = (yyseq . i) . k by A10;

yyseq . i is sequence of REAL by FUNCT_2:66;

hence yseqk . j in REAL by A11, FUNCT_2:5; :: thesis: verum

end;assume j in dom yseqk ; :: thesis: yseqk . j in REAL

then consider i being Element of dom G such that

i = j and

A11: yseqk . j = (yyseq . i) . k by A10;

yyseq . i is sequence of REAL by FUNCT_2:66;

hence yseqk . j in REAL by A11, FUNCT_2:5; :: thesis: verum

yyy is Element of (len yyy) -tuples_on REAL by FINSEQ_2:92;

then reconsider yseqk = yseqk as Element of REAL I by A10, FINSEQ_1:def 3;

now :: thesis: for j being Element of dom G holds yseqk . j = (yyseq . j) . k

hence
ex yseqk being Element of REAL I st Slet j be Element of dom G; :: thesis: yseqk . j = (yyseq . j) . k

j in dom G ;

then j in Seg I by FINSEQ_1:def 3;

then ex i being Element of dom G st

( i = j & yseqk . j = (yyseq . i) . k ) by A10;

hence yseqk . j = (yyseq . j) . k ; :: thesis: verum

end;j in dom G ;

then j in Seg I by FINSEQ_1:def 3;

then ex i being Element of dom G st

( i = j & yseqk . j = (yyseq . i) . k ) by A10;

hence yseqk . j = (yyseq . j) . k ; :: thesis: verum

A12: for k being Element of NAT holds S

A13: now :: thesis: for i0 being Element of NAT st i0 in Seg I holds

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

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

the carrier of (REAL-NS I) = REAL I
by REAL_NS1:def 4;ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 i0 be Element of NAT ; :: thesis: ( i0 in Seg I implies ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 i0 in Seg I ; :: thesis: ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

then reconsider i = i0 as Element of dom G by FINSEQ_1:def 3;

take i = i; :: thesis: ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

consider rseqi being Real_Sequence, seqi being sequence of (G . i) such that

A14: ( rseqi = yyseq . i & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (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;

take rseqi = rseqi; :: thesis: ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

take seqi = seqi; :: thesis: ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

thus ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 A12, A14; :: thesis: verum

end;( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 i0 in Seg I ; :: thesis: ex i being Element of dom G ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

then reconsider i = i0 as Element of dom G by FINSEQ_1:def 3;

take i = i; :: thesis: ex rseqi being Real_Sequence ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

consider rseqi being Real_Sequence, seqi being sequence of (G . i) such that

A14: ( rseqi = yyseq . i & seqi is convergent & rseqi is convergent & lim rseqi = 0 & rseqi = ||.(seqi - (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;

take rseqi = rseqi; :: thesis: ex seqi being sequence of (G . i) st

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

take seqi = seqi; :: thesis: ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (lim seqi)).|| & ( for m being Element of NAT ex seqm being Element of product (carr G) st

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

thus ( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 A12, A14; :: thesis: verum

then reconsider xseq = yseq as sequence of (REAL-NS I) ;

xseq = yseq ;

then consider xseq being sequence of (REAL-NS I), yseq being sequence of (REAL I) such that

A15: xseq = yseq and

A16: for i0 being Element of NAT st i0 in Seg I holds

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

( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 A13;

A17: for i being Nat st i in Seg I holds

ex rseqi being Real_Sequence st

( ( for k being Nat holds rseqi . k = (yseq . k) . i ) & rseqi is convergent & (0* I) . i = lim rseqi )

proof

A20:
product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #)
by Th6;
let i0 be Nat; :: thesis: ( i0 in Seg I implies ex rseqi being Real_Sequence st

( ( for k being Nat holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) )

assume i0 in Seg I ; :: thesis: ex rseqi being Real_Sequence st

( ( for k being Nat holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi )

then consider i being Element of dom G, rseqi being Real_Sequence, seqi being sequence of (G . i) such that

A18: for k being Element of NAT holds rseqi . k = (yseq . k) . i0 and

A19: ( i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 A16;

take rseqi ; :: thesis: ( ( for k being Nat holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi )

thus for k being Nat holds rseqi . k = (yseq . k) . i0 :: thesis: ( rseqi is convergent & (0* I) . i0 = lim rseqi )

end;( ( for k being Nat holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) )

assume i0 in Seg I ; :: thesis: ex rseqi being Real_Sequence st

( ( for k being Nat holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi )

then consider i being Element of dom G, rseqi being Real_Sequence, seqi being sequence of (G . i) such that

A18: for k being Element of NAT holds rseqi . k = (yseq . k) . i0 and

A19: ( i = i0 & seqi is convergent & rseqi is convergent & lim rseqi = (0* I) . i & rseqi = ||.(seqi - (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 A16;

take rseqi ; :: thesis: ( ( for k being Nat holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi )

thus for k being Nat holds rseqi . k = (yseq . k) . i0 :: thesis: ( rseqi is convergent & (0* I) . i0 = lim rseqi )

proof

thus
( rseqi is convergent & (0* I) . i0 = lim rseqi )
by A19; :: thesis: verum
let k be Nat; :: thesis: rseqi . k = (yseq . k) . i0

k in NAT by ORDINAL1:def 12;

hence rseqi . k = (yseq . k) . i0 by A18; :: thesis: verum

end;k in NAT by ORDINAL1:def 12;

hence rseqi . k = (yseq . k) . i0 by A18; :: thesis: verum

now :: thesis: for x being object st x in NAT holds

||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x

then A35:
||.(xseq - (0. (REAL-NS I))).|| = ||.(seq - x0).||
by FUNCT_2:12;||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x

let x be object ; :: thesis: ( x in NAT implies ||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x )

assume x in NAT ; :: thesis: ||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x

then reconsider i = x as Element of NAT ;

reconsider seqimx0 = (seq . i) - x0 as Element of product (carr G) by A20;

then len (yseq . i) = len (normsequence (G,seqimx0)) by Def11;

then dom (yseq . i) = dom (normsequence (G,seqimx0)) by FINSEQ_3:29;

then A34: yseq . i = normsequence (G,seqimx0) by A21, FINSEQ_1:13;

thus ||.(xseq - (0. (REAL-NS I))).|| . x = ||.((xseq - (0. (REAL-NS I))) . i).|| by NORMSP_0:def 4

.= ||.((xseq . i) - (0. (REAL-NS I))).|| by NORMSP_1:def 4

.= ||.(xseq . i).||

.= |.(yseq . i).| by A15, REAL_NS1:1

.= ||.((seq . i) - x0).|| by A34, Th7

.= ||.((seq - x0) . i).|| by NORMSP_1:def 4

.= ||.(seq - x0).|| . x by NORMSP_0:def 4 ; :: thesis: verum

end;assume x in NAT ; :: thesis: ||.(xseq - (0. (REAL-NS I))).|| . x = ||.(seq - x0).|| . x

then reconsider i = x as Element of NAT ;

reconsider seqimx0 = (seq . i) - x0 as Element of product (carr G) by A20;

A21: now :: thesis: for k being Nat st k in dom (normsequence (G,seqimx0)) holds

(normsequence (G,seqimx0)) . k = (yseq . i) . k

len (yseq . i) = I
by CARD_1:def 7;(normsequence (G,seqimx0)) . k = (yseq . i) . k

reconsider mx0 = - x0 as Element of product (carr G) by A20;

let k be Nat; :: thesis: ( k in dom (normsequence (G,seqimx0)) implies (normsequence (G,seqimx0)) . k = (yseq . i) . k )

assume A22: k in dom (normsequence (G,seqimx0)) ; :: thesis: (normsequence (G,seqimx0)) . k = (yseq . i) . k

A23: len G = len (normsequence (G,seqimx0)) by Def11;

then reconsider k0 = k as Element of dom G by A22, FINSEQ_3:29;

k in Seg I by A22, A23, FINSEQ_1:def 3;

then consider k1 being Element of dom G, rseqk1i being Real_Sequence, seqk1i being sequence of (G . k1) such that

A24: for j being Element of NAT holds rseqk1i . j = (yseq . j) . k and

A25: k1 = k and

seqk1i is convergent and

rseqk1i is convergent and

lim rseqk1i = (0* I) . k1 and

A26: rseqk1i = ||.(seqk1i - (lim seqk1i)).|| and

A27: for m being Element of NAT ex seqk1m being Element of product (carr G) st

( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) by A16;

consider seqk0 being sequence of (G . k0) such that

seqk0 is convergent and

A28: y0 . k0 = lim seqk0 and

A29: for m being Element of NAT ex seqm0 being Element of product (carr G) st

( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) by A2;

A30: ex seqm0 being Element of product (carr G) st

( seqm0 = seq . i & seqk0 . i = seqm0 . k0 ) by A29;

len G = len (carr G) by Def4;

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

- x0 = (- 1) * x0 by RLVECT_1:16;

then mx0 . k0 = (- jj) * (lim seqk0) by A1, A20, A28, A32, Lm4;

then - (lim seqk0) = mx0 . k0 by RLVECT_1:16;

then A33: seqimx0 . k0 = (seqk0 . i) - (lim seqk0) by A20, A30, A32, Lm3;

thus (normsequence (G,seqimx0)) . k = the normF of (G . k0) . (seqimx0 . k0) by Def11

.= ||.((seqk0 - (lim seqk0)) . i).|| by A33, NORMSP_1:def 4

.= ||.(seqk1i - (lim seqk1i)).|| . i by A25, A31, NORMSP_0:def 4

.= (yseq . i) . k by A24, A26 ; :: thesis: verum

end;let k be Nat; :: thesis: ( k in dom (normsequence (G,seqimx0)) implies (normsequence (G,seqimx0)) . k = (yseq . i) . k )

assume A22: k in dom (normsequence (G,seqimx0)) ; :: thesis: (normsequence (G,seqimx0)) . k = (yseq . i) . k

A23: len G = len (normsequence (G,seqimx0)) by Def11;

then reconsider k0 = k as Element of dom G by A22, FINSEQ_3:29;

k in Seg I by A22, A23, FINSEQ_1:def 3;

then consider k1 being Element of dom G, rseqk1i being Real_Sequence, seqk1i being sequence of (G . k1) such that

A24: for j being Element of NAT holds rseqk1i . j = (yseq . j) . k and

A25: k1 = k and

seqk1i is convergent and

rseqk1i is convergent and

lim rseqk1i = (0* I) . k1 and

A26: rseqk1i = ||.(seqk1i - (lim seqk1i)).|| and

A27: for m being Element of NAT ex seqk1m being Element of product (carr G) st

( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) by A16;

consider seqk0 being sequence of (G . k0) such that

seqk0 is convergent and

A28: y0 . k0 = lim seqk0 and

A29: for m being Element of NAT ex seqm0 being Element of product (carr G) st

( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) by A2;

A30: ex seqm0 being Element of product (carr G) st

( seqm0 = seq . i & seqk0 . i = seqm0 . k0 ) by A29;

now :: thesis: for x being object st x in NAT holds

seqk1i . x = seqk0 . x

then A31:
seqk1i = seqk0
by A25, FUNCT_2:12;seqk1i . x = seqk0 . x

let x be object ; :: thesis: ( x in NAT implies seqk1i . x = seqk0 . x )

assume x in NAT ; :: thesis: seqk1i . x = seqk0 . x

then reconsider m = x as Element of NAT ;

( ex seqk1m being Element of product (carr G) st

( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) & ex seqm0 being Element of product (carr G) st

( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) ) by A29, A27;

hence seqk1i . x = seqk0 . x by A25; :: thesis: verum

end;assume x in NAT ; :: thesis: seqk1i . x = seqk0 . x

then reconsider m = x as Element of NAT ;

( ex seqk1m being Element of product (carr G) st

( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) & ex seqm0 being Element of product (carr G) st

( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) ) by A29, A27;

hence seqk1i . x = seqk0 . x by A25; :: thesis: verum

len G = len (carr G) by Def4;

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

- x0 = (- 1) * x0 by RLVECT_1:16;

then mx0 . k0 = (- jj) * (lim seqk0) by A1, A20, A28, A32, Lm4;

then - (lim seqk0) = mx0 . k0 by RLVECT_1:16;

then A33: seqimx0 . k0 = (seqk0 . i) - (lim seqk0) by A20, A30, A32, Lm3;

thus (normsequence (G,seqimx0)) . k = the normF of (G . k0) . (seqimx0 . k0) by Def11

.= ||.((seqk0 - (lim seqk0)) . i).|| by A33, NORMSP_1:def 4

.= ||.(seqk1i - (lim seqk1i)).|| . i by A25, A31, NORMSP_0:def 4

.= (yseq . i) . k by A24, A26 ; :: thesis: verum

then len (yseq . i) = len (normsequence (G,seqimx0)) by Def11;

then dom (yseq . i) = dom (normsequence (G,seqimx0)) by FINSEQ_3:29;

then A34: yseq . i = normsequence (G,seqimx0) by A21, FINSEQ_1:13;

thus ||.(xseq - (0. (REAL-NS I))).|| . x = ||.((xseq - (0. (REAL-NS I))) . i).|| by NORMSP_0:def 4

.= ||.((xseq . i) - (0. (REAL-NS I))).|| by NORMSP_1:def 4

.= ||.(xseq . i).||

.= |.(yseq . i).| by A15, REAL_NS1:1

.= ||.((seq . i) - x0).|| by A34, Th7

.= ||.((seq - x0) . i).|| by NORMSP_1:def 4

.= ||.(seq - x0).|| . x by NORMSP_0:def 4 ; :: thesis: verum

0* I = 0. (REAL-NS I) by REAL_NS1:def 4;

then ( xseq is convergent & lim xseq = 0. (REAL-NS I) ) by A15, A17, REAL_NS1:11;

then ( ||.(seq - x0).|| is convergent & lim ||.(seq - x0).|| = 0 ) by A35, Lm7;

hence ( seq is convergent & lim seq = x0 ) by Lm7; :: thesis: verum