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

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in COMPLEX & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in COMPLEX & S₁[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H₁( Element of NAT ) -> Element of COMPLEX = (seq_id (vseq . $1)) . i;
consider cseqi being Complex_Sequence such that
A3: for n being Element of NAT holds cseqi . n = H₁(n) from COMSEQ_1:sch 1();
A4: cseqi is convergent

proof

now

let e be Real; :: thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e )
assume A5: e > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e
thus ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e :: thesis: verum

proof

consider k being Element of NAT such that
A6: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A5, CSSPACE3:10;
take k ; :: thesis: for m being Element of NAT st k <= m holds
|.((cseqi . m) - (cseqi . k)).| < e
let m be Element of NAT ; :: thesis: ( k <= m implies |.((cseqi . m) - (cseqi . k)).| < e )
assume A7: k <= m ; :: thesis: |.((cseqi . m) - (cseqi . k)).| < e
||.((vseq . m) - (vseq . k)).|| = sup (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Th3;
then A8: sup (rng |.(seq_id ((vseq . m) - (vseq . k))).|) < e by A6, A7;
seq_id ((vseq . m) - (vseq . k)) is bounded by Def1;
then |.(seq_id ((vseq . m) - (vseq . k))).| is bounded by Lm9;
then A9: |.(seq_id ((vseq . m) - (vseq . k))).| . i <= sup (rng |.(seq_id ((vseq . m) - (vseq . k))).|) by Lm2;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th3
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by CSSPACE:3 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by VALUED_1:1
.= ((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 |.((cseqi . m) - (cseqi . k)).| = |.(seq_id ((vseq . m) - (vseq . k))).| . i by VALUED_1:18;
hence |.((cseqi . m) - (cseqi . k)).| < e by A8, A9, XXREAL_0:2; :: thesis: verum

end;

end;

hence cseqi is convergent by COMSEQ_3:46; :: thesis: verum

end;

take y = lim cseqi; :: thesis: ( y in COMPLEX & S₁[x,y] )
thus ( y in COMPLEX & S₁[x,y] ) by A3, A4; :: thesis: verum

end;

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

A11: now

let i be Element of NAT ; :: thesis: ex cseqi being Complex_Sequence st
( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi )
reconsider x = i as set ;
ex i0 being Element of NAT st
( x = i0 & ex cseqi being Complex_Sequence st
( ( for n being Element of 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 Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi ) ; :: thesis: verum

end;

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

proof

let e be Real; :: thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A13: e > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
consider k being Element of NAT such that
A14: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A13, CSSPACE3:10;
A15: for m, n being Element of NAT st n >= k & m >= k holds
( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & sup (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e )

proof

let m, n be Element of NAT ; :: thesis: ( n >= k & m >= k implies ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & sup (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) )
assume A16: ( n >= k & m >= k ) ; :: thesis: ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & sup (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e )
||.((vseq . n) - (vseq . m)).|| < e by A14, A16;
then A17: the norm of Complex_linfty_Space . ((vseq . n) - (vseq . m)) < e by CLVECT_1:def 10;
seq_id ((vseq . n) - (vseq . m)) is bounded by Def1;
hence ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & sup (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) by A17, Def2, Lm9; :: thesis: verum

end;

A18: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 Element of NAT ; :: thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 )
A19: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))

proof

let m, k be Element of NAT ; :: thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th3;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by CSSPACE:3; :: thesis: verum

end;

now

let i be Element of NAT ; :: thesis: for rseq being Real_Sequence st ( for m being Element of 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 )
consider cseqi being Complex_Sequence such that
A20: ( ( for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i ) & cseqi is convergent & tseq . i = lim cseqi ) by A11;

now

let rseq be Real_Sequence; :: thesis: ( ( for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ) implies ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) )
assume A21: for m being Element of NAT holds rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i ; :: thesis: ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i )

A22: now

let m be Element of NAT ; :: thesis: rseq . m = |.((cseqi . m) - ((seq_id (vseq . n)) . i)).|
A23: seq_id ((vseq . m) - (vseq . n)) = (seq_id (vseq . m)) - (seq_id (vseq . n)) by A19;
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, Lm12
.= |.((cseqi . m) - ((seq_id (vseq . n)) . i)).| by A20 ; :: thesis: verum

end;

|.((tseq . i) - ((seq_id (vseq . n)) . i)).| = |.((tseq - (seq_id (vseq . n))) . i).| by Lm12
.= |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| by CSSPACE:3
.= |.((seq_id tseq) - (seq_id (vseq . n))).| . i by VALUED_1:18 ;
hence ( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) by A20, A22, CSSPACE3:1; :: thesis: verum

end;

hence for rseq being Real_Sequence st ( for m being Element of 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: verum

end;

hence for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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: verum

end;

for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )

proof

let n be Element of NAT ; :: thesis: ( n >= k implies ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A24: n >= k ; :: thesis: ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
A25: for i being Element of NAT holds |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e

proof

let i be Element of NAT ; :: thesis: |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e
deffunc H₁( Element of NAT ) -> Element of REAL = |.(seq_id ((vseq . $1) - (vseq . n))).| . i;
consider rseq being Real_Sequence such that
A26: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
A27: rseq is convergent by A18, A26;
A28: lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i by A18, A26;
for m being Element of NAT st m >= k holds
rseq . m <= e

proof

let m be Element of NAT ; :: thesis: ( m >= k implies rseq . m <= e )
assume m >= k ; :: thesis: rseq . m <= e
then A29: ( |.(seq_id ((vseq . m) - (vseq . n))).| is bounded & sup (rng |.(seq_id ((vseq . m) - (vseq . n))).|) <= e ) by A15, A24;
then A30: |.(seq_id ((vseq . m) - (vseq . n))).| . i <= sup (rng |.(seq_id ((vseq . m) - (vseq . n))).|) by Lm2;
rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A26;
hence rseq . m <= e by A29, A30, XXREAL_0:2; :: thesis: verum

end;

hence |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e by A27, A28, RSSPACE2:6; :: thesis: verum

end;

|.((seq_id tseq) - (seq_id (vseq . n))).| is bounded

proof

A31: 0 + 0 < 1 + e by A13;
A32: 0 + e < 1 + e by XREAL_1:10;

now

let i be Element of NAT ; :: thesis: |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1
|.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e by A25;
then |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| <= e by VALUED_1:18;
hence |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| < e + 1 by A32, XXREAL_0:2; :: thesis: verum

end;

then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A31, COMSEQ_2:8;
hence |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded by Lm9; :: thesis: verum

end;

hence ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) by A25, Lm1; :: thesis: verum

end;

hence ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) ; :: thesis: verum

end;

A33: seq_id tseq is bounded

proof

consider m being Element of NAT such that
A34: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= 1 ) by A12;
A35: |.((seq_id tseq) - (seq_id (vseq . m))).| is bounded by A34;
seq_id (vseq . m) is bounded by Def1;
then A36: |.(seq_id (vseq . m)).| is bounded by Lm9;
set a = |.((seq_id tseq) - (seq_id (vseq . m))).|;
set b = |.(seq_id (vseq . m)).|;
set d = |.(seq_id tseq).|;
A37: |.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).| is bounded by A35, A36;
A38: for i being Element of NAT holds |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i

proof

let i be Element of NAT ; :: thesis: |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i
A39: |.((seq_id tseq) - (seq_id (vseq . m))).| . i = |.(((seq_id tseq) + (- (seq_id (vseq . m)))) . i).| by VALUED_1:18
.= |.(((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)).| by VALUED_1:1
.= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by VALUED_1:8
.= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
A40: |.(seq_id (vseq . m)).| . i = |.((seq_id (vseq . m)) . i).| by VALUED_1:18;
|.(seq_id tseq).| . i = |.((seq_id tseq) . i).| by VALUED_1:18;
then (|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i) <= |.((seq_id tseq) - (seq_id (vseq . m))).| . i by A39, A40, COMPLEX1:145;
then ((|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i)) + (|.(seq_id (vseq . m)).| . i) <= (|.((seq_id tseq) - (seq_id (vseq . m))).| . i) + (|.(seq_id (vseq . m)).| . i) by XREAL_1:8;
hence |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i by SEQ_1:11; :: thesis: verum

end;

|.(seq_id tseq).| is bounded

proof

reconsider r = (sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 as real number ;
0 <= sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))

proof

A41: (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . 1 = (|.((seq_id tseq) - (seq_id (vseq . m))).| . 1) + (|.(seq_id (vseq . m)).| . 1) by SEQ_1:11;
|.((seq_id tseq) - (seq_id (vseq . m))).| . 1 = |.(((seq_id tseq) - (seq_id (vseq . m))) . 1).| by VALUED_1:18;
then A42: 0 <= |.((seq_id tseq) - (seq_id (vseq . m))).| . 1 by COMPLEX1:132;
|.(seq_id (vseq . m)).| . 1 = |.((seq_id (vseq . m)) . 1).| by VALUED_1:18;
then 0 <= |.(seq_id (vseq . m)).| . 1 by COMPLEX1:132;
then 0 + 0 <= (|.((seq_id tseq) - (seq_id (vseq . m))).| . 1) + (|.(seq_id (vseq . m)).| . 1) by A42;
hence 0 <= sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by A37, A41, Lm2; :: thesis: verum

end;

then A43: 0 + 0 < (sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 ;
A44: (sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 0 < (sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 by XREAL_1:10;

now

let i be Element of NAT ; :: thesis: |.((seq_id tseq) . i).| < r
A45: |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i by A38;
(|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i <= sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by A37, Lm2;
then A46: |.(seq_id tseq).| . i <= sup (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by A45, XXREAL_0:2;
|.(seq_id tseq).| . i = |.((seq_id tseq) . i).| by VALUED_1:18;
hence |.((seq_id tseq) . i).| < r by A44, A46, XXREAL_0:2; :: thesis: verum

end;

then seq_id tseq is bounded by A43, COMSEQ_2:8;
hence |.(seq_id tseq).| is bounded by Lm9; :: thesis: verum

end;

hence seq_id tseq is bounded by Lm10; :: thesis: verum

end;

A47: tseq in the_set_of_ComplexSequences by CSSPACE:def 1;
then reconsider tv = tseq as Point of Complex_linfty_Space by A33, Def1;
ex tv being Point of Complex_linfty_Space st
for e1 being Real st e1 > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1

proof

take tv ; :: thesis: for e1 being Real st e1 > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1
let e1 be Real; :: thesis: ( e1 > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1 )
assume A48: e1 > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e1
set e = e1 / 2;
A49: e1 / 2 > 0 by A48, XREAL_1:217;
A50: e1 / 2 < e1 by A48, XREAL_1:218;
consider m being Element of NAT such that
A51: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 ) by A12, A49;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e1 )
assume A52: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e1
reconsider u = tseq as VECTOR of Complex_linfty_Space by A33, A47, Def1;
A53: sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 by A51, A52;
reconsider v = vseq . n as VECTOR of Complex_linfty_Space ;
seq_id (u - v) = u - v by Th3;
then sup (rng |.(seq_id (u - v)).|) = sup (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) by Th3;
then A54: the norm of Complex_linfty_Space . (u - v) <= e1 / 2 by A53, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:47
.= ||.(tv - (vseq . n)).|| by CLVECT_1:104 ;
then ||.((vseq . n) - tv).|| <= e1 / 2 by A54, CLVECT_1:def 10;
hence ||.((vseq . n) - tv).|| < e1 by A50, XXREAL_0:2; :: thesis: verum

end;

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

end;

hence vseq is convergent by CLVECT_1:def 16; :: thesis: verum