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 } )

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

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

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

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 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 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 } ) 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 }

end;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;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

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

hence
x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
by A6, Th54; :: thesis: verum
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

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ; :: thesis: verum

end;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

hence
ex n being Nat st
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;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

for n1, n2 being Nat st n <= n1 & n <= n2 holds

s . (n1,n2) in B ; :: thesis: verum

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