let M be non empty MetrSpace; :: thesis: for p being Point of M
for x being Point of (TopSpaceMetr M)
for s being Function of [:NAT,NAT:],(TopSpaceMetr M) st x = p holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } )
let p be Point of M; :: thesis: for x being Point of (TopSpaceMetr M)
for s being Function of [:NAT,NAT:],(TopSpaceMetr M) st x = p holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } )
let x be Point of (TopSpaceMetr M); :: thesis: for s being Function of [:NAT,NAT:],(TopSpaceMetr M) st x = p holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } )
let s be Function of [:NAT,NAT:],(TopSpaceMetr M); :: thesis: ( x = p implies ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } ) )
assume A1: x = p ; :: thesis: ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } )
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } )

proof

hereby :: thesis: ( ( for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } ) implies x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) )

assume A2: x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) ; :: thesis: for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m }

hereby :: thesis: verum

let m be non zero Nat; :: thesis: ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m }
set B = { q where q is Point of M : dist (p,q) < 1 / m } ;
A3: { q where q is Point of M : dist (p,q) < 1 / m } = Ball (p,(1 / m)) by METRIC_1:def 14;
ex y being Point of M st
( y = x & Balls x = { (Ball (y,(1 / m))) where m is Nat : m <> 0 } ) by FRECHET:def 1;
then A4: { q where q is Point of M : dist (p,q) < 1 / m } in Balls x by A3, A1;
Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by CARDFIL3:6;
hence ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } by A2, A4, Th54; :: thesis: verum

end;

end;

assume A5: for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } ; :: thesis: x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
A6: Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by CARDFIL3:6;
for B being Element of Balls x ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B

proof

let B be Element of Balls x; :: thesis: ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B
consider y being Point of M such that
A7: y = x and
A8: Balls x = { (Ball (y,(1 / m))) where m is Nat : m <> 0 } by FRECHET:def 1;
B in Balls x ;
then consider m0 being Nat such that
A9: B = Ball (y,(1 / m0)) and
A10: m0 <> 0 by A8;
consider n0 being Nat such that
A11: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m0 } by A5, A10;
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in B

proof

let n1, n2 be Nat; :: thesis: ( n0 <= n1 & n0 <= n2 implies s . (n1,n2) in B )
assume ( n0 <= n1 & n0 <= n2 ) ; :: thesis: s . (n1,n2) in B
then s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m0 } by A11;
hence s . (n1,n2) in B by A9, A1, A7, METRIC_1:def 14; :: thesis: verum

end;

hence ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B ; :: thesis: verum

end;

hence x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by A6, Th54; :: thesis: verum

end;

hence ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } ) ; :: thesis: verum