let T be non empty TopSpace; :: thesis: 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; :: thesis: 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 }

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: 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

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; :: thesis: 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 }
; :: thesis: verumnow :: thesis: 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 }

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 }
;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 ; :: thesis: ( 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:] } ; :: thesis: 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; :: thesis: verum

end;assume x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] } ; :: thesis: 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; :: thesis: verum

now :: thesis: 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:] }

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:] }
;x in { M where M is Subset of the carrier of T : s " M in Frechet_Filter [:NAT,NAT:] }

let x be object ; :: thesis: ( 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 } ; :: thesis: 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; :: thesis: verum

end;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 } ; :: thesis: 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; :: thesis: verum

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; :: thesis: verum