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 that
A1: f is continuous and
A2: 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 A3: P in f " B ; :: thesis: P is open
thus P is open :: thesis: verum

proof

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

end;

end;

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