let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( ( for x being Element of NAT holds lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ) iff Rseq is convergent_in_cod2 )
hereby :: thesis: ( Rseq is convergent_in_cod2 implies for x being Element of NAT holds lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} )
assume A1: for x being Element of NAT holds lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ; :: thesis: Rseq is convergent_in_cod2
now :: thesis: for m being Element of NAT holds ProjMap1 (Rseq,m) is convergent
let m be Element of NAT ; :: thesis: ProjMap1 (Rseq,m) is convergent
not lim_filter ((ProjMap1 ((# Rseq),m)),(Frechet_Filter NAT)) is empty by A1;
then consider r being Element of (TopSpaceMetr RealSpace) such that
A2: r in lim_filter ((ProjMap1 ((# Rseq),m)),(Frechet_Filter NAT)) ;
A3: r in lim_f (ProjMap1 ((# 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
|.(((ProjMap1 (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
|.(((ProjMap1 (Rseq,m)) . n) - r1).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap1 (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
(ProjMap1 ((# 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
|.(((ProjMap1 (Rseq,m)) . n) - r1).| < e :: thesis: verum
proof
take i ; :: thesis: for n being Nat st i <= n holds
|.(((ProjMap1 (Rseq,m)) . n) - r1).| < e
let j be Nat; :: thesis: ( i <= j implies |.(((ProjMap1 (Rseq,m)) . j) - r1).| < e )
assume i <= j ; :: thesis: |.(((ProjMap1 (Rseq,m)) . j) - r1).| < e
then (ProjMap1 ((# Rseq),m)) . j in Ball (y,e) by A9, A10;
then (ProjMap1 ((# Rseq),m)) . j in ].(y - e),(y + e).[ by FRECHET:7;
hence |.(((ProjMap1 (Rseq,m)) . j) - r1).| < e by A7, FCONT_3:1; :: thesis: verum
end;
end;
hence ProjMap1 (Rseq,m) is convergent by SEQ_2:def 6; :: thesis: verum
end;
hence Rseq is convergent_in_cod2 ; :: thesis: verum
end;
assume A11: Rseq is convergent_in_cod2 ; :: thesis: for x being Element of NAT holds lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}
now :: thesis: for x being Element of NAT holds not lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) is empty
let x be Element of NAT ; :: thesis: not lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) is empty
consider r being Real such that
A12: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((ProjMap1 (Rseq,x)) . m) - r).| < p by A11, SEQ_2:def 6;
reconsider r1 = r as Point of (TopSpaceMetr RealSpace) by XREAL_0:def 1;
A13: 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
(ProjMap1 ((# 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
(ProjMap1 ((# Rseq),x)) . j in b
consider y being Point of RealSpace such that
A14: y = r1 and
A15: 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 A15;
then consider n0 being Nat such that
A16: b = Ball (y,(1 / n0)) and
A17: n0 <> 0 ;
( 0 < n0 & 0 * n0 < 1 ) by A17;
then consider n1 being Nat such that
A18: for m being Nat st n1 <= m holds
|.(((ProjMap1 (Rseq,x)) . m) - r).| < 1 / n0 by A12, XREAL_1:81;
now :: thesis: ex n1 being Nat st
for j being Nat st n1 <= j holds
(ProjMap1 ((# Rseq),x)) . j in b
take n1 = n1; :: thesis: for j being Nat st n1 <= j holds
(ProjMap1 ((# Rseq),x)) . j in b
hereby :: thesis: verum
let j be Nat; :: thesis: ( n1 <= j implies (ProjMap1 ((# Rseq),x)) . j in b )
assume n1 <= j ; :: thesis: (ProjMap1 ((# Rseq),x)) . j in b
then A19: |.(((ProjMap1 (Rseq,x)) . j) - r).| < 1 / n0 by A18;
(ProjMap1 (Rseq,x)) . j = r + (((ProjMap1 (Rseq,x)) . j) - r) ;
then (ProjMap1 (Rseq,x)) . j in ].(r - (1 / n0)),(r + (1 / n0)).[ by A19, FCONT_3:3;
hence (ProjMap1 ((# Rseq),x)) . j in b by A14, A16, FRECHET:7; :: thesis: verum
end;
end;
hence ex i being Nat st
for j being Nat st i <= j holds
(ProjMap1 ((# Rseq),x)) . j in b ; :: thesis: verum
end;
then not lim_f (ProjMap1 ((# Rseq),x)) is empty by A13, CARDFIL2:97;
hence not lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) is empty ; :: thesis: verum
end;
hence for x being Element of NAT holds lim_filter ((ProjMap1 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ; :: thesis: verum