let G be RealNormSpace-Sequence; :: thesis: for seq being sequence of ()
for x0 being Point of ()
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 (); :: thesis: for x0 being Point of ()
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 (); :: 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 S1[ 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 S1[i,yyseqi]
proof
let i be Element of dom G; :: thesis: ex yyseqi being Element of Funcs (NAT,REAL) st S1[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 ;
hence ex yyseqi being Element of Funcs (NAT,REAL) st S1[i,yyseqi] by A4, A5, A6; :: thesis: verum
end;
consider yyseq being Function of (dom G),(Funcs (NAT,REAL)) such that
A7: for i being Element of dom G holds S1[i,yyseq . i] from reconsider I = len G as Element of NAT ;
defpred S2[ 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 S2[k,yseqk]
proof
let k be Element of NAT ; :: thesis: ex yseqk being Element of REAL I st S2[k,yseqk]
defpred S3[ 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 S3[k,x]
proof
let j be Nat; :: thesis: ( j in Seg I implies ex x being object st S3[j,x] )
assume j in Seg I ; :: thesis: ex x being object st S3[j,x]
then reconsider i = j as Element of dom G by FINSEQ_1:def 3;
take (yyseq . i) . k ; :: thesis: S3[j,(yyseq . i) . k]
thus S3[j,(yyseq . i) . k] ; :: thesis: verum
end;
consider yseqk being FinSequence such that
A10: ( dom yseqk = Seg I & ( for j being Nat st j in Seg I holds
S3[j,yseqk . j] ) ) from
now :: thesis: for j being Nat st j in dom yseqk holds
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 ; :: thesis: verum
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 ;
now :: thesis: for j being Element of dom G holds yseqk . j = (yyseq . j) . k
let 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;
hence ex yseqk being Element of REAL I st S2[k,yseqk] ; :: thesis: verum
end;
consider yseq being sequence of (REAL I) such that
A12: for k being Element of NAT holds S2[k,yseq . k] from
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 ) ) )
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 ; :: thesis: verum
end;
the carrier of () = REAL I by REAL_NS1:def 4;
then reconsider xseq = yseq as sequence of () ;
xseq = yseq ;
then consider xseq being sequence of (), 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: ( 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 )
proof
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;
thus ( rseqi is convergent & (0* I) . i0 = lim rseqi ) by A19; :: thesis: verum
end;
A20: product G = NORMSTR(# (product (carr G)),(),[:():],[:():],() #) by Th6;
now :: thesis: for x being object st x in NAT holds
||.(xseq - (0. ())).|| . x = ||.(seq - x0).|| . x
let x be object ; :: thesis: ( x in NAT implies ||.(xseq - (0. ())).|| . x = ||.(seq - x0).|| . x )
assume x in NAT ; :: thesis: ||.(xseq - (0. ())).|| . 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
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 ;
k in Seg I by ;
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
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 ;
hence seqk1i . x = seqk0 . x by A25; :: thesis: verum
end;
then A31: seqk1i = seqk0 by ;
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
.= ||.(seqk1i - (lim seqk1i)).|| . i by
.= (yseq . i) . k by ; :: thesis: verum
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 ;
thus ||.(xseq - (0. ())).|| . x = ||.((xseq - (0. ())) . i).|| by NORMSP_0:def 4
.= ||.((xseq . i) - (0. ())).|| by NORMSP_1:def 4
.= ||.(xseq . i).||
.= |.(yseq . i).| by
.= ||.((seq . i) - x0).|| by
.= ||.((seq - x0) . i).|| by NORMSP_1:def 4
.= ||.(seq - x0).|| . x by NORMSP_0:def 4 ; :: thesis: verum
end;
then A35: ||.(xseq - (0. ())).|| = ||.(seq - x0).|| by FUNCT_2:12;
0* I = 0. () by REAL_NS1:def 4;
then ( xseq is convergent & lim xseq = 0. () ) by ;
then ( ||.(seq - x0).|| is convergent & lim ||.(seq - x0).|| = 0 ) by ;
hence ( seq is convergent & lim seq = x0 ) by Lm7; :: thesis: verum