let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( ( for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ) 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)),(Frechet_Filter NAT)) <> {} )

assume A1: for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ; :: 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)),(Frechet_Filter NAT)) is empty by A1;
then consider r being Element of (TopSpaceMetr RealSpace) such that
A2: r in lim_filter ((ProjMap2 ((# Rseq),m)),(Frechet_Filter NAT)) ;
A3: r in lim_f (ProjMap2 ((# Rseq),m)) by A2;
A4: Balls r is basis of (BOOL2F (NeighborhoodSystem r)) 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 A6, PCOMPS_1:1;
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 A4, A3, CARDFIL2:97;
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 A9, A10;
then (ProjMap2 ((# Rseq),m)) . j in ].(y - e),(y + e).[ by FRECHET:7;
hence |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e by A7, FCONT_3:1; :: 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)),(Frechet_Filter NAT)) <> {}

now :: thesis: for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}

let x be Element of NAT ; :: thesis: lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}
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 A13, SEQ_2:def 6;
reconsider r1 = r as Point of (TopSpaceMetr RealSpace) by XREAL_0:def 1;
A15: Balls r1 is basis of (BOOL2F (NeighborhoodSystem r1)) 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 A14, XREAL_1:81;

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 A21, FCONT_3:3;
hence (ProjMap2 ((# Rseq),x)) . j in b by A16, A18, FRECHET:7; :: 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 A15, CARDFIL2:97;
hence lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ; :: thesis: verum

end;

hence for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ; :: thesis: verum