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: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₁[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 , 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₃[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 :: thesis:

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 sequence of REAL by FUNCT_2:66;
hence yseqk . j in REAL by A11, FUNCT_2:5; :: thesis:

end;

then reconsider yyy = yseqk as FinSequence of REAL by FINSEQ_2:12;
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:

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 sequence of (REAL I) such that
A12: for k being Element of NAT holds S₂[k,yseq . k] from FUNCT_2:sch 3(A8);

A13: now :: thesis:

let i0 be Element of NAT ; :: thesis:
assume 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
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:
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; :: thesis:

end;

reconsider xseq = yseq as sequence of (REAL-NS I) by REAL_NS1:def 4;
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

let i0 be Nat; :: thesis:
assume i0 in Seg I ; :: thesis:
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:
thus for k being Nat holds rseqi . k = (yseq . k) . i0 :: thesis:

proof

let k be Nat; :: thesis:
k in NAT by ORDINAL1:def 12;
hence rseqi . k = (yseq . k) . i0 by A18; :: thesis:

end;

thus ( rseqi is convergent & (0* I) . i0 = lim rseqi ) by A19; :: thesis:

end;

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

now :: thesis:

let x be object ; :: 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 A20;

A21: now :: thesis:

reconsider mx0 = - x0 as Element of product (carr G) by A20;
let k be Nat; :: thesis:
assume A22: k in dom (normsequence (G,seqimx0)) ; :: thesis:
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:

let x be object ; :: 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 A29, A27;
hence seqk1i . x = seqk0 . x by A25; :: thesis:

end;

then A31: seqk1i = seqk0 by A25, FUNCT_2:12;
len G = len (carr G) by PRVECT_1:def 11;
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:

end;

len (yseq . i) = I by CARD_1:def 7;
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:

end;

then A35: ||.(xseq - (0. (REAL-NS I))).|| = ||.(seq - x0).|| by FUNCT_2:12;
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: