let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T

for x being Point of T holds

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for x being Point of T holds

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite )

let x be Point of T; :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite )

for x being Point of T holds

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for x being Point of T holds

( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite )

let x be Point of T; :: thesis: ( x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) iff for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite )

hereby :: thesis: ( ( for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite ) implies x in lim_filter (s,(Frechet_Filter [:NAT,NAT:])) )

assume A2:
for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite
; :: thesis: x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))assume A1:
x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
; :: thesis: for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite

end;now :: thesis: for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite

hence
for A being a_neighborhood of x holds [:NAT,NAT:] \ (s " A) is finite
; :: thesis: verumlet A be a_neighborhood of x; :: thesis: [:NAT,NAT:] \ (s " A) is finite

ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B by A1, Th45;

hence [:NAT,NAT:] \ (s " A) is finite by Th1; :: thesis: verum

end;ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B by A1, Th45;

hence [:NAT,NAT:] \ (s " A) is finite by Th1; :: thesis: verum

now :: thesis: for A being a_neighborhood of x ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B

hence
x in lim_filter (s,(Frechet_Filter [:NAT,NAT:]))
by Th45; :: thesis: verumlet A be a_neighborhood of x; :: thesis: ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B

A3: dom s = [:NAT,NAT:] by FUNCT_2:def 1;

[:NAT,NAT:] \ (s " A) is finite by A2;

hence ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B by A3, RELAT_1:132, Th2; :: thesis: verum

end;A3: dom s = [:NAT,NAT:] by FUNCT_2:def 1;

[:NAT,NAT:] \ (s " A) is finite by A2;

hence ex B being finite Subset of [:NAT,NAT:] st s " A = [:NAT,NAT:] \ B by A3, RELAT_1:132, Th2; :: thesis: verum