let T, S be non empty TopSpace; :: thesis: for f being Function of T,S
for B being Subset-Family of S st f is continuous & B is open holds
f " B is open
let f be Function of T,S; :: thesis: for B being Subset-Family of S st f is continuous & B is open holds
f " B is open
let B be Subset-Family of S; :: thesis: ( f is continuous & B is open implies f " B is open )
assume A1: ( f is continuous & B is open ) ; :: thesis: f " B is open
for P being Subset of T st P in f " B holds
P is open

proof

let P be Subset of T; :: thesis: ( P in f " B implies P is open )
assume A2: P in f " B ; :: thesis: P is open
thus P is open :: thesis: verum

proof

consider C being Subset of S such that
A3: ( C in B & P = f " C ) by A2, FUNCT_2:def 10;
reconsider C = C as Subset of S ;
A4: [#] S <> {} ;
C is open by A1, A3, TOPS_2:def 1;
hence P is open by A1, A3, A4, TOPS_2:55; :: thesis: verum

end;

end;

hence f " B is open by TOPS_2:def 1; :: thesis: verum