let T, S be TopSpace; :: thesis:
let f be Function of T,S; :: thesis:

end;

given B being Basis of T such that A2: for V being Subset of T st V in B holds
f .: V is open ; :: thesis:

let A be Subset of T; :: thesis:
set Y = { G where G is Subset of T : ( G in B & G c= A ) } ;
{ G where G is Subset of T : ( G in B & G c= A ) } c= bool the carrier of T

let g be object ; :: according to TARSKI:def 3 :: thesis:
assume g in { G where G is Subset of T : ( G in B & G c= A ) } ; :: thesis:
then ex G being Subset of T st
( g = G & G in B & G c= A ) ;
hence g in bool the carrier of T ; :: thesis:

end;

then reconsider Y = { G where G is Subset of T : ( G in B & G c= A ) } as Subset-Family of T ;
set Z = { (f .: G) where G is Subset of T : G in Y } ;
{ (f .: G) where G is Subset of T : G in Y } c= bool the carrier of S

let h be object ; :: according to TARSKI:def 3 :: thesis:
assume h in { (f .: G) where G is Subset of T : G in Y } ; :: thesis:
then ex G being Subset of T st
( h = f .: G & G in Y ) ;
hence h in bool the carrier of S ; :: thesis:

end;

then reconsider Z = { (f .: G) where G is Subset of T : G in Y } as Subset-Family of S ;
A7: for P being Subset of S st P in Z holds
P is open

let P be Subset of S; :: thesis:
assume P in Z ; :: thesis:
then consider G1 being Subset of T such that
A5: ( P = f .: G1 & G1 in Y ) ;
ex G2 being Subset of T st
( G1 = G2 & G2 in B & G2 c= A ) by A5;
hence P is open by A2, A5; :: thesis:

end;

end;