let G be RealNormSpace-Sequence; :: thesis:
let seq be sequence of (product G); :: thesis:
let x0 be Point of (product G); :: thesis:
let y0 be Element of product (carr G); :: thesis:
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:
defpred S₁[ 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₁[i,yyseqi]

let i be Element of dom G; :: thesis:
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:11;
( ||.(seqi - (lim seqi)).|| is convergent & lim ||.(seqi - (lim seqi)).|| = 0 ) by A4, Lm8;
hence ex yyseqi being Element of Funcs NAT ,REAL st S₁[i,yyseqi] by A4, A5, A6; :: thesis:

end;

consider yyseq being Function of (dom G),(Funcs NAT ,REAL ) such that
A7: for i being Element of dom G holds S₁[i,yyseq . i] from FUNCT_2:sch 3(A3);
reconsider I = len G as Element of NAT ;
defpred S₂[ 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₂[k,yseqk]

proof

let k be Element of NAT ; :: thesis:
defpred S₃[ set , set ] 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 set st S₃[k,x]

proof

let j be Nat; :: thesis:
assume j in Seg I ; :: thesis:
then reconsider i = j as Element of dom G by FINSEQ_1:def 3;
take (yyseq . i) . k ; :: thesis:
thus S₃[j,(yyseq . i) . k] ; :: thesis:

end;

consider yseqk being FinSequence such that
A10: ( dom yseqk = Seg I & ( for j being Nat st j in Seg I holds
S₃[j,yseqk . j] ) ) from FINSEQ_1:sch 1(A9);

now

let j be Nat; :: thesis:
assume j in dom yseqk ; :: thesis:
then consider i being Element of dom G such that
i = j and
A11: yseqk . j = (yyseq . i) . k by A10;
yyseq . i is Function of NAT ,REAL by FUNCT_2:121;
hence yseqk . j in REAL by A11, FUNCT_2:7; :: thesis:

end;

then reconsider yyy = yseqk as FinSequence of REAL by FINSEQ_2:14;
yyy is Element of (len yyy) -tuples_on REAL by FINSEQ_2:110;
then reconsider yseqk = yseqk as Element of REAL I by A10, FINSEQ_1:def 3;

now

let j be Element of dom G; :: thesis:
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:

end;

hence ex yseqk being Element of REAL I st S₂[k,yseqk] ; :: thesis:

end;

consider yseq being Function of NAT ,(REAL I) such that
A12: for k being Element of NAT holds S₂[k,yseq . k] from FUNCT_2:sch 3(A8);

A13: now

let i0 be Element of NAT ; :: thesis:
assume A14: i0 in Seg I ; :: thesis:
then reconsider i = i0 as Element of dom G by FINSEQ_1:def 3;
take i = i; :: thesis:
consider rseqi being Real_Sequence, seqi being sequence of (G . i) such that
A15: ( 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:
take seqi = seqi; :: thesis:
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, A15, FUNCOP_1:13; :: thesis:

end;

the carrier of (REAL-NS I) = REAL I by REAL_NS1:def 4;
then reconsider xseq = yseq as sequence of (REAL-NS I) ;
xseq = yseq ;
then consider xseq being sequence of (REAL-NS I), yseq being Function of NAT ,(REAL I) such that
A16: xseq = yseq and
A17: 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;
A18: for i being Element of NAT st i in Seg I holds
ex rseqi being Real_Sequence st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i ) & rseqi is convergent & (0* I) . i = lim rseqi )

proof

let i0 be Element of NAT ; :: thesis:
assume i0 in Seg I ; :: thesis:
then 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 A17;
hence ex rseqi being Real_Sequence st
( ( for k being Element of NAT holds rseqi . k = (yseq . k) . i0 ) & rseqi is convergent & (0* I) . i0 = lim rseqi ) ; :: thesis:

end;

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

now

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Element of NAT ;
reconsider seqimx0 = (seq . i) - x0 as Element of product (carr G) by A19;

A20: now

reconsider mx0 = - x0 as Element of product (carr G) by A19;
let k be Nat; :: thesis:
assume A21: k in dom (normsequence G,seqimx0) ; :: thesis:
A22: len G = len (normsequence G,seqimx0) by Def11;
then reconsider k0 = k as Element of dom G by A21, FINSEQ_3:31;
k in Seg I by A21, A22, FINSEQ_1:def 3;
then consider k1 being Element of dom G, rseqk1i being Real_Sequence, seqk1i being sequence of (G . k1) such that
A23: for j being Element of NAT holds rseqk1i . j = (yseq . j) . k and
A24: k1 = k and
seqk1i is convergent and
rseqk1i is convergent and
lim rseqk1i = (0* I) . k1 and
A25: rseqk1i = ||.(seqk1i - (lim seqk1i)).|| and
A26: for m being Element of NAT ex seqk1m being Element of product (carr G) st
( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) by A17;
consider seqk0 being sequence of (G . k0) such that
seqk0 is convergent and
A27: y0 . k0 = lim seqk0 and
A28: for m being Element of NAT ex seqm0 being Element of product (carr G) st
( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) by A2;
A29: ex seqm0 being Element of product (carr G) st
( seqm0 = seq . i & seqk0 . i = seqm0 . k0 ) by A28;

now

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
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 A28, A26;
hence seqk1i . x = seqk0 . x by A24; :: thesis:

end;

then A30: seqk1i = seqk0 by A24, FUNCT_2:18;
len G = len (carr G) by Def4;
then A31: dom G = dom (carr G) by FINSEQ_3:31;
- x0 = (- 1) * x0 by RLVECT_1:29;
then mx0 . k0 = (- 1) * (lim seqk0) by A1, A19, A27, A31, Lm4;
then - (lim seqk0) = mx0 . k0 by RLVECT_1:29;
then A32: seqimx0 . k0 = (seqk0 . i) - (lim seqk0) by A19, A29, A31, Lm3;
thus (normsequence G,seqimx0) . k = the normF of (G . k0) . (seqimx0 . k0) by Def11
.= ||.((seqk0 - (lim seqk0)) . i).|| by A32, NORMSP_1:def 7
.= ||.(seqk1i - (lim seqk1i)).|| . i by A24, A30, NORMSP_0:def 4
.= (yseq . i) . k by A23, A25 ; :: thesis:

end;

len (yseq . i) = I by FINSEQ_1:def 18;
then len (yseq . i) = len (normsequence G,seqimx0) by Def11;
then dom (yseq . i) = dom (normsequence G,seqimx0) by FINSEQ_3:31;
then A33: yseq . i = normsequence G,seqimx0 by A20, FINSEQ_1:17;
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 7
.= ||.(xseq . i).|| by RLVECT_1:26
.= |.(yseq . i).| by A16, REAL_NS1:1
.= ||.((seq . i) - x0).|| by A33, Th7
.= ||.((seq - x0) . i).|| by NORMSP_1:def 7
.= ||.(seq - x0).|| . x by NORMSP_0:def 4 ; :: thesis:

end;

then A34: ||.(xseq - (0. (REAL-NS I))).|| = ||.(seq - x0).|| by FUNCT_2:18;
0* I = 0. (REAL-NS I) by REAL_NS1:def 4;
then ( xseq is convergent & lim xseq = 0. (REAL-NS I) ) by A16, A18, REAL_NS1:11;
then ( ||.(seq - x0).|| is convergent & lim ||.(seq - x0).|| = 0 ) by A34, Lm8;
hence ( seq is convergent & lim seq = x0 ) by Lm8; :: thesis: