let T be non empty TopSpace; for s being Function of [:NAT,NAT:], the carrier of T holds filter_image (s,(Frechet_Filter [:NAT,NAT:])) = { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
let s be Function of [:NAT,NAT:], the carrier of T; filter_image (s,(Frechet_Filter [:NAT,NAT:])) = { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
set X = { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } ;
set Y = { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } ;
{ M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } = { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
proof
now for x being object st x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } holds
x in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } let x be
object ;
( x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } implies x in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } )assume
x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] }
;
x in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } then consider M being
Subset of the
carrier of
T such that A1:
x = M
and A2:
s " M in Frechet_Filter [:NAT,NAT:]
;
ex
A being
finite Subset of
[:NAT,NAT:] st
s " M = [:NAT,NAT:] \ A
by Th41, A2;
hence
x in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
by A1;
verum end;
then A3:
{ M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } c= { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
;
now for x being object st x in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } holds
x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } let x be
object ;
( x in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } implies x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } )assume
x in { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
;
x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } then consider M being
Subset of the
carrier of
T such that A4:
x = M
and A5:
ex
A being
finite Subset of
[:NAT,NAT:] st
s " M = [:NAT,NAT:] \ A
;
s " M in Frechet_Filter [:NAT,NAT:]
by A5, Th41;
hence
x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] }
by A4;
verum end;
then
{ M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A } c= { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] }
;
hence
{ M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } = { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
by A3;
verum
end;
hence
filter_image (s,(Frechet_Filter [:NAT,NAT:])) = { M where M is Subset of the carrier of T : ex A being finite Subset of [:NAT,NAT:] st s " M = [:NAT,NAT:] \ A }
; verum