let vseq be sequence of 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 rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & $2 = lim rseqi ) );
A2: for x being set st x in NAT holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

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

proof

now

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

proof

e is Real by XREAL_0:def 1;
then 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, RSSPACE3:10;
take k ; :: thesis: for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
let m be Element of NAT ; :: thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume A7: k <= m ; :: thesis: abs ((rseqi . m) - (rseqi . k)) < e
||.((vseq . m) - (vseq . k)).|| = sup (rng (abs (seq_id ((vseq . m) - (vseq . k))))) by Th3;
then A8: sup (rng (abs (seq_id ((vseq . m) - (vseq . k))))) < e by A6, A7;
seq_id ((vseq . m) - (vseq . k)) is bounded by Def1;
then abs (seq_id ((vseq . m) - (vseq . k))) is bounded ;
then A9: (abs (seq_id ((vseq . m) - (vseq . k)))) . i <= sup (rng (abs (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 RSSPACE:3 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:11
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:14
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (rseqi . m) - (rseqi . k) by A3 ;
then abs ((rseqi . m) - (rseqi . k)) = (abs (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:16;
hence abs ((rseqi . m) - (rseqi . k)) < e by A8, A9, XXREAL_0:2; :: thesis: verum

end;

end;

hence rseqi is convergent by SEQ_4:58; :: thesis: verum

end;

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

end;

consider f being Function of NAT ,REAL 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 Real_Sequence ;

A11: now

let i be Element of NAT ; :: thesis: ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
ex i0 being Element of NAT st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A10;
hence ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; :: 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
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & sup (rng (abs ((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
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & sup (rng (abs ((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
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & sup (rng (abs ((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, RSSPACE3:10;
A15: for m, n being Element of NAT st n >= k & m >= k holds
( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & sup (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e )

proof

let m, n be Element of NAT ; :: thesis: ( n >= k & m >= k implies ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & sup (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) )
assume A16: ( n >= k & m >= k ) ; :: thesis: ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & sup (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e )
A17: ||.((vseq . n) - (vseq . m)).|| < e by A14, A16;
seq_id ((vseq . n) - (vseq . m)) is bounded by Def1;
hence ( abs (seq_id ((vseq . n) - (vseq . m))) is bounded & sup (rng (abs (seq_id ((vseq . n) - (vseq . m))))) < e ) by A17, Def2; :: 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 = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((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 = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((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 RSSPACE: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 = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i )
consider rseqi being Real_Sequence such that
A20: ( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) by A11;

now

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

A22: now

let m be Element of NAT ; :: thesis: rseq . m = abs ((rseqi . 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 = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A21
.= abs ((seq_id ((vseq . m) - (vseq . n))) . i) by SEQ_1:16
.= abs (((seq_id (vseq . m)) . i) - ((seq_id (vseq . n)) . i)) by A23, RFUNCT_2:6
.= abs ((rseqi . m) - ((seq_id (vseq . n)) . i)) by A20 ; :: thesis: verum

end;

abs ((tseq . i) - ((seq_id (vseq . n)) . i)) = abs ((tseq - (seq_id (vseq . n))) . i) by RFUNCT_2:6
.= abs (((seq_id tseq) - (seq_id (vseq . n))) . i) by RSSPACE:3
.= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i by SEQ_1:16 ;
hence ( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) by A20, A22, RSSPACE3:1; :: thesis: verum

end;

hence for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((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 = (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) holds
( rseq is convergent & lim rseq = (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i ) ; :: thesis: verum

end;

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

proof

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

proof

let i be Element of NAT ; :: thesis: (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e
deffunc H₁( Element of NAT ) -> Element of REAL = (abs (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 = (abs ((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: ( abs (seq_id ((vseq . m) - (vseq . n))) is bounded & sup (rng (abs (seq_id ((vseq . m) - (vseq . n))))) <= e ) by A15, A24;
then A30: (abs (seq_id ((vseq . m) - (vseq . n)))) . i <= sup (rng (abs (seq_id ((vseq . m) - (vseq . n))))) by Lm2;
rseq . m = (abs (seq_id ((vseq . m) - (vseq . n)))) . i by A26;
hence rseq . m <= e by A29, A30, XXREAL_0:2; :: thesis: verum

end;

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

end;

abs ((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: abs (((seq_id tseq) - (seq_id (vseq . n))) . i) < e + 1
A33: (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i <= e by A25;
(abs ((seq_id tseq) - (seq_id (vseq . n)))) . i = abs (((seq_id tseq) - (seq_id (vseq . n))) . i) by SEQ_1:16;
hence abs (((seq_id tseq) - (seq_id (vseq . n))) . i) < e + 1 by A32, A33, XXREAL_0:2; :: thesis: verum

end;

then (seq_id tseq) - (seq_id (vseq . n)) is bounded by A31, SEQ_2:15;
hence abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded ; :: thesis: verum

end;

hence ( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & sup (rng (abs ((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
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & sup (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e ) ; :: thesis: verum

end;

A34: seq_id tseq is bounded

proof

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

proof

let i be Element of NAT ; :: thesis: (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i
A40: (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i = abs (((seq_id tseq) + (- (seq_id (vseq . m)))) . i) by SEQ_1:16
.= abs (((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)) by SEQ_1:11
.= abs (((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))) by SEQ_1:14
.= abs (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)) ;
A41: (abs (seq_id (vseq . m))) . i = abs ((seq_id (vseq . m)) . i) by SEQ_1:16;
(abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) by SEQ_1:16;
then ((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i) <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i by A40, A41, COMPLEX1:145;
then (((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i)) + ((abs (seq_id (vseq . m))) . i) <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . i) + ((abs (seq_id (vseq . m))) . i) by XREAL_1:8;
hence (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i by SEQ_1:11; :: thesis: verum

end;

abs (seq_id tseq) is bounded

proof

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

proof

A42: ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . 1 = ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1) + ((abs (seq_id (vseq . m))) . 1) by SEQ_1:11;
(abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 = abs (((seq_id tseq) - (seq_id (vseq . m))) . 1) by SEQ_1:16;
then A43: 0 <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1 by COMPLEX1:132;
(abs (seq_id (vseq . m))) . 1 = abs ((seq_id (vseq . m)) . 1) by SEQ_1:16;
then 0 <= (abs (seq_id (vseq . m))) . 1 by COMPLEX1:132;
then 0 + 0 <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . 1) + ((abs (seq_id (vseq . m))) . 1) by A43;
hence 0 <= sup (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by A38, A42, Lm2; :: thesis: verum

end;

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

now

let i be Element of NAT ; :: thesis: abs ((seq_id tseq) . i) < r
A46: (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i by A39;
((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i <= sup (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by A38, Lm2;
then A47: (abs (seq_id tseq)) . i <= sup (rng ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))))) by A46, XXREAL_0:2;
(abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) by SEQ_1:16;
hence abs ((seq_id tseq) . i) < r by A45, A47, XXREAL_0:2; :: thesis: verum

end;

then seq_id tseq is bounded by A44, SEQ_2:15;
hence abs (seq_id tseq) is bounded ; :: thesis: verum

end;

hence seq_id tseq is bounded by SEQM_3:70; :: thesis: verum

end;

A48: tseq in the_set_of_RealSequences by RSSPACE:def 1;
then reconsider tv = tseq as Point of linfty_Space by A34, Def1;
take tv ; :: according to NORMSP_1:def 9 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= ||.((vseq . b₃) - tv).|| ) )
let e1 be Real; :: thesis: ( e1 <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not e1 <= ||.((vseq . b₂) - tv).|| ) )
assume A49: e1 > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not e1 <= ||.((vseq . b₂) - tv).|| )
set e = e1 / 2;
A50: e1 / 2 > 0 by A49, XREAL_1:217;
A51: e1 / 2 < e1 by A49, XREAL_1:218;
consider m being Element of NAT such that
A52: for n being Element of NAT st n >= m holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is bounded & sup (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 ) by A12, A50;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e1 )
assume A53: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e1
reconsider u = tseq as VECTOR of linfty_Space by A34, A48, Def1;
A54: sup (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 by A52, A53;
reconsider v = vseq . n as VECTOR of linfty_Space ;
seq_id (u - v) = u - v by Th3;
then sup (rng (abs (seq_id (u - v)))) = sup (rng (abs ((seq_id tseq) - (seq_id (vseq . n))))) by Th3;
then A55: the norm of linfty_Space . (u - v) <= e1 / 2 by A54, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:47
.= ||.(tv - (vseq . n)).|| by NORMSP_1:6 ;
hence ||.((vseq . n) - tv).|| < e1 by A51, A55, XXREAL_0:2; :: thesis: verum

end;

hence ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not e1 <= ||.((vseq . b₂) - tv).|| ) ; :: thesis: verum