let Rseq be Function of ,REAL; :: thesis: ( ( for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),) <> {} ) iff Rseq is convergent_in_cod1 )
hereby :: thesis: ( Rseq is convergent_in_cod1 implies for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),) <> {} )
assume A1: for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),) <> {} ; :: thesis: Rseq is convergent_in_cod1
now :: thesis: for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent
let m be Element of NAT ; :: thesis: ProjMap2 (Rseq,m) is convergent
not lim_filter ((ProjMap2 ((# Rseq),m)),) is empty by A1;
then consider r being Element of such that
A2: r in lim_filter ((ProjMap2 ((# Rseq),m)),) ;
A3: r in lim_f (ProjMap2 ((# Rseq),m)) by A2;
A4: Balls r is basis of () by CARDFIL3:6;
reconsider r1 = r as Real ;
now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e )

assume 0 < e ; :: thesis: ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

then consider m1 being Nat such that
A5: not m1 is zero and
A6: 1 / m1 < e by Th5;
consider y being Point of RealSpace such that
A7: y = r and
A8: Balls r = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
A9: Ball (y,(1 / m1)) c= Ball (y,e) by ;
Ball (y,(1 / m1)) in Balls r by A8, A5;
then consider i being Nat such that
A10: for j being Nat st i <= j holds
(ProjMap2 ((# Rseq),m)) . j in Ball (y,(1 / m1)) by ;
thus ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e :: thesis: verum
proof
take i ; :: thesis: for n being Nat st i <= n holds
|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

let j be Nat; :: thesis: ( i <= j implies |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e )
assume i <= j ; :: thesis: |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e
then (ProjMap2 ((# Rseq),m)) . j in Ball (y,e) by ;
then (ProjMap2 ((# Rseq),m)) . j in ].(y - e),(y + e).[ by FRECHET:7;
hence |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e by ; :: thesis: verum
end;
end;
hence ProjMap2 (Rseq,m) is convergent by SEQ_2:def 6; :: thesis: verum
end;
hence Rseq is convergent_in_cod1 ; :: thesis: verum
end;
assume A13: Rseq is convergent_in_cod1 ; :: thesis: for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),) <> {}
now :: thesis: for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),) <> {}
let x be Element of NAT ; :: thesis: lim_filter ((ProjMap2 ((# Rseq),x)),) <> {}
consider r being Real such that
A14: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((ProjMap2 (Rseq,x)) . m) - r).| < p by ;
reconsider r1 = r as Point of by XREAL_0:def 1;
A15: Balls r1 is basis of () by CARDFIL3:6;
for b being Element of Balls r1 ex i being Nat st
for j being Nat st i <= j holds
(ProjMap2 ((# Rseq),x)) . j in b
proof
let b be Element of Balls r1; :: thesis: ex i being Nat st
for j being Nat st i <= j holds
(ProjMap2 ((# Rseq),x)) . j in b

consider y being Point of RealSpace such that
A16: y = r1 and
A17: Balls r1 = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
b in { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by A17;
then consider n0 being Nat such that
A18: b = Ball (y,(1 / n0)) and
A19: n0 <> 0 ;
( 0 < n0 & 0 * n0 < 1 ) by A19;
then consider n1 being Nat such that
A20: for m being Nat st n1 <= m holds
|.(((ProjMap2 (Rseq,x)) . m) - r).| < 1 / n0 by ;
now :: thesis: ex n1 being Nat st
for j being Nat st n1 <= j holds
(ProjMap2 ((# Rseq),x)) . j in b
take n1 = n1; :: thesis: for j being Nat st n1 <= j holds
(ProjMap2 ((# Rseq),x)) . j in b

hereby :: thesis: verum
let j be Nat; :: thesis: ( n1 <= j implies (ProjMap2 ((# Rseq),x)) . j in b )
assume n1 <= j ; :: thesis: (ProjMap2 ((# Rseq),x)) . j in b
then A21: |.(((ProjMap2 (Rseq,x)) . j) - r).| < 1 / n0 by A20;
(ProjMap2 (Rseq,x)) . j = r + (((ProjMap2 (Rseq,x)) . j) - r) ;
then (ProjMap2 (Rseq,x)) . j in ].(r - (1 / n0)),(r + (1 / n0)).[ by ;
hence (ProjMap2 ((# Rseq),x)) . j in b by ; :: thesis: verum
end;
end;
hence ex i being Nat st
for j being Nat st i <= j holds
(ProjMap2 ((# Rseq),x)) . j in b ; :: thesis: verum
end;
then lim_f (ProjMap2 ((# Rseq),x)) <> {} by ;
hence lim_filter ((ProjMap2 ((# Rseq),x)),) <> {} ; :: thesis: verum
end;
hence for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),) <> {} ; :: thesis: verum