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 A1: ( 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 ) ) ) ) ) ; :: thesis:
reconsider I = len G as Element of NAT ;
A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;
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]

proof

let i be Element of dom G; :: thesis:
consider seqi being sequence of (G . i) such that
A4: ( seqi is convergent & y0 . i = lim seqi & ( for m being Element of NAT ex Sm being Element of product (carr G) st
( Sm = seq . m & seqi . m = Sm . i ) ) ) by A1;
set rseqi = ||.(seqi - (lim seqi)).||;
A5: ( ||.(seqi - (lim seqi)).|| is convergent & lim ||.(seqi - (lim seqi)).|| = 0 ) by A4, Lm8;
||.(seqi - (lim seqi)).|| is Element of Funcs NAT ,REAL by FUNCT_2:11;
hence ex yyseqi being Element of Funcs NAT ,REAL st S₁[i,yyseqi] by A4, A5; :: thesis:

end;

consider yyseq being Function of (dom G),(Funcs NAT ,REAL ) such that
A6: for i being Element of dom G holds S₁[i,yyseq . i] from FUNCT_2:sch 3(A3);
defpred S₂[ Element of NAT , Element of REAL I] means for i being Element of dom G holds (yyseq . i) . $1 = $2 . i;
A7: 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
A11: ( i = j & 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(A7);
the carrier of (REAL-NS I) = REAL I by REAL_NS1:def 4;
then reconsider xseq = yseq as sequence of (REAL-NS I) ;
A13: xseq = yseq ;

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 A6;
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;

then consider xseq being sequence of (REAL-NS I), yseq being Function of NAT ,(REAL I) such that
A16: ( xseq = yseq & ( 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 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 A16;
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;

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

proof

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 A2;
A19: yseq . i = normsequence G,seqimx0

proof

len (yseq . i) = I by FINSEQ_1:def 18;
then len (yseq . i) = len (normsequence G,seqimx0) by Def11;
then A20: dom (yseq . i) = dom (normsequence G,seqimx0) by FINSEQ_3:31;

now

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;
consider seqk0 being sequence of (G . k0) such that
A23: ( seqk0 is convergent & y0 . k0 = lim seqk0 & ( for m being Element of NAT ex seqm0 being Element of product (carr G) st
( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) ) ) by A1;
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
A24: ( ( for j being Element of NAT holds rseqk1i . j = (yseq . j) . k ) & k1 = k & seqk1i is convergent & rseqk1i is convergent & lim rseqk1i = (0* I) . k1 & rseqk1i = ||.(seqk1i - (lim seqk1i)).|| & ( for m being Element of NAT ex seqk1m being Element of product (carr G) st
( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) ) ) by A16;

now

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider m = x as Element of NAT ;
A25: ex seqk1m being Element of product (carr G) st
( seqk1m = seq . m & seqk1i . m = seqk1m . k1 ) by A24;
ex seqm0 being Element of product (carr G) st
( seqm0 = seq . m & seqk0 . m = seqm0 . k0 ) by A23;
hence seqk1i . x = seqk0 . x by A24, A25; :: thesis:

end;

then A26: seqk1i = seqk0 by A24, FUNCT_2:18;
consider seqm0 being Element of product (carr G) such that
A27: ( seqm0 = seq . i & seqk0 . i = seqm0 . k0 ) by A23;
reconsider mx0 = - x0 as Element of product (carr G) by A2;
len G = len (carr G) by Def4;
then A28: dom G = dom (carr G) by FINSEQ_3:31;
- x0 = (- 1) * x0 by RLVECT_1:29;
then mx0 . k0 = (- 1) * (lim seqk0) by A1, A2, A23, A28, Lm4;
then - (lim seqk0) = mx0 . k0 by RLVECT_1:29;
then A29: seqimx0 . k0 = (seqk0 . i) - (lim seqk0) by A2, A27, A28, Lm3;
thus (normsequence G,seqimx0) . k = the norm of (G . k0) . (seqimx0 . k0) by Def11
.= ||.((seqk0 - (lim seqk0)) . i).|| by A29, NORMSP_1:def 7
.= ||.(seqk1i - (lim seqk1i)).|| . i by A24, A26, NORMSP_1:def 10
.= (yseq . i) . k by A24 ; :: thesis:

end;

hence yseq . i = normsequence G,seqimx0 by A20, FINSEQ_1:17; :: thesis:

end;

thus ||.(xseq - (0. (REAL-NS I))).|| . x = ||.((xseq - (0. (REAL-NS I))) . i).|| by NORMSP_1:def 10
.= ||.((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 A19, Th7
.= ||.((seq - x0) . i).|| by NORMSP_1:def 7
.= ||.(seq - x0).|| . x by NORMSP_1:def 10 ; :: thesis:

end;

hence ||.(xseq - (0. (REAL-NS I))).|| = ||.(seq - x0).|| by FUNCT_2:18; :: thesis:

end;

then ( ||.(seq - x0).|| is convergent & lim ||.(seq - x0).|| = 0 ) by A18, Lm8;
hence ( seq is convergent & lim seq = x0 ) by Lm8; :: thesis: