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),(Frechet_Filter NAT).)) = { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M }
let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M }
set X = { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } ;
set Y = { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } ;
{ M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } = { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M }
proof
now :: thesis: for x being object st x in { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } holds
x in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M }
let x be object ; :: thesis: ( x in { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } implies x in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } )
assume x in { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } ; :: thesis: x in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M }
then consider M being Subset of the carrier of T such that
A1: x = M and
A2: s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) ;
ex n being Nat st square-uparrow n c= s " M by Th42, A2;
hence x in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } by A1; :: thesis: verum
end;
then A3: { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } c= { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } ;
now :: thesis: for x being object st x in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } holds
x in { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) }
let x be object ; :: thesis: ( x in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } implies x in { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } )
assume x in { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } ; :: thesis: x in { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) }
then consider M being Subset of the carrier of T such that
A4: x = M and
A5: ex n being Nat st square-uparrow n c= s " M ;
s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by A5, Th42;
hence x in { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } by A4; :: thesis: verum
end;
then { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } c= { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } ;
hence { M where M is Subset of the carrier of T : s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) } = { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } by A3; :: thesis: verum
end;
hence filter_image (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = { M where M is Subset of the carrier of T : ex n being Nat st square-uparrow n c= s " M } ; :: thesis: verum