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();
take y = lim cseqi; :: thesis: ( y in COMPLEX & S₁[x,y] )

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 A4: 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
A5: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, 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 A6: k <= m ; :: thesis: |.((cseqi . m) - (cseqi . k)).| < e
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 A7: |.((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 Lm9;
then A8: |.(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 Th3;
then upper_bound (rng |.(seq_id ((vseq . m) - (vseq . k))).|) < e by A5, A6;
hence |.((cseqi . m) - (cseqi . k)).| < e by A8, A7, XXREAL_0:2; :: thesis: verum

end;

end;

then cseqi is convergent by COMSEQ_3:46;
hence ( y in COMPLEX & S₁[x,y] ) by A3; :: thesis: verum

end;

consider f being Function of NAT ,COMPLEX such that
A9: 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 ;

A10: 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 A9;
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;

A11: 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 & upper_bound (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 & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A12: 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 & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
consider k being Element of NAT such that
A13: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A12, CSSPACE3:10;
A14: for m, n being Element of 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 Element of NAT ; :: thesis: ( n >= k & m >= k implies ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e ) )
assume ( n >= k & m >= k ) ; :: thesis: ( |.(seq_id ((vseq . n) - (vseq . m))).| is bounded & upper_bound (rng |.(seq_id ((vseq . n) - (vseq . m))).|) < e )
then ||.((vseq . n) - (vseq . m)).|| < e by A13;
then A15: 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 A15, Def2, Lm9; :: thesis: verum

end;

A16: 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 )
A17: 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
A18: for n being Element of NAT holds cseqi . n = (seq_id (vseq . n)) . i and
A19: ( cseqi is convergent & tseq . i = lim cseqi ) by A10;

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 A20: 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 )

A21: now

let m be Element of NAT ; :: thesis: rseq . m = |.((cseqi . m) - ((seq_id (vseq . n)) . i)).|
A22: seq_id ((vseq . m) - (vseq . n)) = (seq_id (vseq . m)) - (seq_id (vseq . n)) by A17;
thus rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A20
.= |.((seq_id ((vseq . m) - (vseq . n))) . i).| by VALUED_1:18
.= |.(((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)).| by A22, Lm12
.= |.((cseqi . m) - ((seq_id (vseq . n)) . i)).| by A18 ; :: 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 A19, A21, 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 & upper_bound (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 & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) )
assume A23: n >= k ; :: thesis: ( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e )
A24: 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
A25: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
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 )
A27: rseq . m = |.(seq_id ((vseq . m) - (vseq . n))).| . i by A25;
assume A28: m >= k ; :: thesis: rseq . m <= e
then |.(seq_id ((vseq . m) - (vseq . n))).| is bounded by A14, A23;
then A29: |.(seq_id ((vseq . m) - (vseq . n))).| . i <= upper_bound (rng |.(seq_id ((vseq . m) - (vseq . n))).|) by Lm2;
upper_bound (rng |.(seq_id ((vseq . m) - (vseq . n))).|) <= e by A14, A23, A28;
hence rseq . m <= e by A29, A27, XXREAL_0:2; :: thesis: verum

end;

( rseq is convergent & lim rseq = |.((seq_id tseq) - (seq_id (vseq . n))).| . i ) by A16, A25;
hence |.((seq_id tseq) - (seq_id (vseq . n))).| . i <= e by A26, RSSPACE2:6; :: thesis: verum

end;

A30: 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 A24;
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 A30, XXREAL_0:2; :: thesis: verum

end;

then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A12, 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 A24, Lm1, Lm9; :: 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 & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e ) ; :: thesis: verum

end;

A31: seq_id tseq is bounded

proof

consider m being Element of NAT such that
A32: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= 1 ) by A11;
A33: |.((seq_id tseq) - (seq_id (vseq . m))).| is bounded by A32;
set d = |.(seq_id tseq).|;
set b = |.(seq_id (vseq . m)).|;
set a = |.((seq_id tseq) - (seq_id (vseq . m))).|;
seq_id (vseq . m) is bounded by Def1;
then A34: |.(seq_id (vseq . m)).| is bounded by Lm9;
A35: 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
A36: ( |.(seq_id (vseq . m)).| . i = |.((seq_id (vseq . m)) . i).| & |.(seq_id tseq).| . i = |.((seq_id tseq) . i).| ) by VALUED_1:18;
|.((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)).| ;
then (|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i) <= |.((seq_id tseq) - (seq_id (vseq . m))).| . i by A36, 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 = (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 as real number ;
|.(seq_id (vseq . m)).| . 1 = |.((seq_id (vseq . m)) . 1).| by VALUED_1:18;
then A37: 0 <= |.(seq_id (vseq . m)).| . 1 by COMPLEX1:132;
A38: (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 0 < (upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|))) + 1 by XREAL_1:10;

A39: now

let i be Element of NAT ; :: thesis: |.((seq_id tseq) . i).| < r
( |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i & (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) ) by A33, A34, A35, Lm2;
then A40: |.(seq_id tseq).| . i <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by XXREAL_0:2;
|.(seq_id tseq).| . i = |.((seq_id tseq) . i).| by VALUED_1:18;
hence |.((seq_id tseq) . i).| < r by A38, A40, XXREAL_0:2; :: thesis: verum

end;

|.((seq_id tseq) - (seq_id (vseq . m))).| . 1 = |.(((seq_id tseq) - (seq_id (vseq . m))) . 1).| by VALUED_1:18;
then ( (|.((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) & 0 <= |.((seq_id tseq) - (seq_id (vseq . m))).| . 1 ) by COMPLEX1:132, SEQ_1:11;
then 0 <= upper_bound (rng (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|)) by A33, A34, A37, Lm2;
then seq_id tseq is bounded by A39, 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;

A41: tseq in the_set_of_ComplexSequences by CSSPACE:def 1;
then reconsider tv = tseq as Point of Complex_linfty_Space by A31, 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 A42: 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;
consider m being Element of NAT such that
A43: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded & upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 ) by A11, A42, XREAL_1:217;
A44: e1 / 2 < e1 by A42, XREAL_1:218;

now

reconsider u = tseq as VECTOR of Complex_linfty_Space by A31, A41, Def1;
let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e1 )
assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e1
then A45: upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 by A43;
reconsider v = vseq . n as VECTOR of Complex_linfty_Space ;
seq_id (u - v) = u - v by Th3;
then upper_bound (rng |.(seq_id (u - v)).|) = upper_bound (rng |.((seq_id tseq) - (seq_id (vseq . n))).|) by Th3;
then A46: the normF of Complex_linfty_Space . (u - v) <= e1 / 2 by A45, 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 A46;
hence ||.((vseq . n) - tv).|| < e1 by A44, 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