let vseq be sequence of Complex_linfty_Space; :: thesis:
assume A1: vseq is Cauchy_sequence_by_Norm ; :: thesis:
defpred S₁[ object , object ] means ex i being Nat st
( $1 = i & ex cseqi being Complex_Sequence st
( ( for n being Nat holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & $2 = lim cseqi ) );
A2: for x being object st x in NAT holds
ex y being object st
( y in COMPLEX & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Nat ;
deffunc H₁( Nat) -> set = (seq_id (vseq . $1)) . i;
consider cseqi being Complex_Sequence such that
A3: for n being Nat holds cseqi . n = H₁(n) from COMSEQ_1:sch 1();
take lim cseqi ; :: thesis:
thus lim cseqi in COMPLEX by XCMPLX_0:def 2; :: thesis:

now :: thesis:

let e be Real; :: thesis:
assume A4: e > 0 ; :: thesis:
thus ex k being Nat st
for m being Nat st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e :: thesis:

proof

reconsider ee = e as Real ;
consider k being Nat such that
A5: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < ee by A1, A4, CSSPACE3:8;
take k ; :: thesis:
let m be Nat; :: thesis:
assume A6: k <= m ; :: thesis:
A7: i in NAT by ORDINAL1:def 12;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by VALUED_1:1, A7
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by VALUED_1:8
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (cseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (cseqi . m) - (cseqi . k) by A3 ;
then A8: |.((cseqi . m) - (cseqi . k)).| = |.(seq_id ((vseq . m) - (vseq . k))).| . i by VALUED_1:18;
seq_id ((vseq . m) - (vseq . k)) is bounded by Def1;
then |.(seq_id ((vseq . m) - (vseq . k))).| is bounded by Lm8;
then A9: |.(seq_id ((vseq . m) - (vseq . k))).| . i <= upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Lm2;
||.((vseq . m) - (vseq . k)).|| = upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Th2;
then upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) < e by A5, A6;
hence |.((cseqi . m) - (cseqi . k)).| < e by A9, A8, XXREAL_0:2; :: thesis:

end;

then cseqi is convergent by COMSEQ_3:46;
hence S₁[x, lim cseqi] by A3; :: thesis:

end;

consider f being sequence of COMPLEX such that
A10: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
reconsider tseq = f as Complex_Sequence ;

A11: now :: thesis:

let i be Nat; :: thesis:
reconsider x = i as set ;
i in NAT by ORDINAL1:def 12;
then ex i0 being Nat st
( x = i0 & ex cseqi being Complex_Sequence st
( ( for n being Nat holds cseqi . n = (seq_id (vseq . n)) . i0 ) & cseqi is convergent & f . x = lim cseqi ) ) by A10;
hence ex cseqi being Complex_Sequence st
( ( for n being Nat holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi ) ; :: thesis:

end;

A12: for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )

proof

let e be Real; :: thesis:
assume A13: e > 0 ; :: thesis:
consider k being Nat such that
A14: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A13, CSSPACE3:8;
A15: for m, n being Nat st n >= k & m >= k holds
( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e )

proof

let m, n be Nat; :: thesis:
assume ( n >= k & m >= k ) ; :: thesis:
then ||.((vseq . n) - (vseq . m)).|| < e by A14;
then A16: the normF of Complex_linfty_Space . ((vseq . n) - (vseq . m)) < e ;
seq_id ((vseq . n) - (vseq . m)) is bounded by Def1;
hence ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) by A16, Def2, Lm8; :: thesis:

end;

A17: for n, i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i )

proof

let n be Nat; :: thesis:
A18: for m, k being Nat holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))

proof

let m, k be Nat; :: thesis:
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th2;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) ; :: thesis:

end;

now :: thesis:

let i be Nat; :: thesis:
consider cseqi being Complex_Sequence such that
A19: for n being Nat holds cseqi . n = (seq_id (vseq . n)) . i and
A20: ( cseqi is convergent & tseq . i = lim cseqi ) by A11;

now :: thesis:

let rseq be Real_Sequence; :: thesis:
assume A21: for m being Nat holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ; :: thesis:

A22: now :: thesis:

let m be Nat; :: thesis:
A23: seq_id ((vseq . m) - (vseq . n)) = (seq_id (vseq . m)) - (seq_id (vseq . n)) by A18;
thus rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A21
.= |.((seq_id ((vseq . m) - (vseq . n))) . i).| by VALUED_1:18
.= |.(((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)).| by A23, Lm11
.= |.((cseqi . m) - ((seq_id (vseq . n)) . i)).| by A19 ; :: thesis:

end;

end;

hence for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) ; :: thesis:

end;

hence for i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) holds
( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) ; :: thesis:

end;

for n being Nat st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )

proof

let n be Nat; :: thesis:
assume A24: n >= k ; :: thesis:
A25: for i being Nat holds |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e

proof

let i be Nat; :: thesis:
deffunc H₁( Nat) -> set = |.(seq_id ((vseq . $1) - (vseq . n))).| . i;
consider rseq being Real_Sequence such that
A26: for m being Nat holds rseq . m = H₁(m) from SEQ_1:sch 1();
A27: for m being Nat st m >= k holds
rseq . m <= e

proof

end;

( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) by A17, A26;
hence |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e by A27, RSSPACE2:5; :: thesis:

end;

A31: 0 + e < 1 + e by XREAL_1:8;

now :: thesis:

end;

then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A13, COMSEQ_2:8;
hence ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) by A25, Lm1, Lm8; :: thesis:

end;

hence ex k being Nat st
for n being Nat st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) ; :: thesis:

end;

A32: seq_id tseq is bounded

proof

proof

end;

|.(seq_id tseq).| is bounded

proof

A41: now :: thesis:

end;

end;

hence seq_id tseq is bounded by Lm9; :: thesis:

end;

A43: tseq in the_set_of_ComplexSequences by FUNCT_2:8;
then reconsider tv = tseq as Point of Complex_linfty_Space by A32, Def1;
ex tv being Point of Complex_linfty_Space st
for e1 being Real st e1 > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e1

proof

take tv ; :: thesis:
let e1 be Real; :: thesis:
assume A44: e1 > 0 ; :: thesis:
set e = e1 / 2;
reconsider ee = e1 / 2 as Real ;
consider m being Nat such that
A45: for n being Nat st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= ee ) by A12, A44;
A46: e1 / 2 < e1 by A44, XREAL_1:216;

now :: thesis:

reconsider u = tseq as VECTOR of Complex_linfty_Space by A32, A43, Def1;
let n be Nat; :: thesis:
assume n >= m ; :: thesis:
then A47: upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 by A45;
reconsider v = vseq . n as VECTOR of Complex_linfty_Space ;
seq_id (u - v) = u - v by Th2;
then upper_bound (rng |.(seq_id (u - v)).|) = upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) by Th2;
then A48: the normF of Complex_linfty_Space . (u - v) <= e1 / 2 by A47, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by CLVECT_1:103 ;
then ||.((vseq . n) - tv).|| <= e1 / 2 by A48;
hence ||.((vseq . n) - tv).|| < e1 by A46, XXREAL_0:2; :: thesis:

end;

hence ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e1 ; :: thesis:

end;

hence vseq is convergent by CLVECT_1:def 15; :: thesis: