let X be non empty TopSpace; :: thesis: for M being non empty MetrSpace
for f being Function of X,() st f is continuous holds
for r being Real
for u being Element of M
for P being Subset of () st P = Ball (u,r) holds
f " P is open

let M be non empty MetrSpace; :: thesis: for f being Function of X,() st f is continuous holds
for r being Real
for u being Element of M
for P being Subset of () st P = Ball (u,r) holds
f " P is open

let f be Function of X,(); :: thesis: ( f is continuous implies for r being Real
for u being Element of M
for P being Subset of () st P = Ball (u,r) holds
f " P is open )

assume A1: f is continuous ; :: thesis: for r being Real
for u being Element of M
for P being Subset of () st P = Ball (u,r) holds
f " P is open

let r be Real; :: thesis: for u being Element of M
for P being Subset of () st P = Ball (u,r) holds
f " P is open

let u be Element of M; :: thesis: for P being Subset of () st P = Ball (u,r) holds
f " P is open

let P be Subset of (); :: thesis: ( P = Ball (u,r) implies f " P is open )
reconsider P9 = P as Subset of () ;
assume P = Ball (u,r) ; :: thesis: f " P is open
then ( [#] () <> {} & P9 is open ) by TOPMETR:14;
hence f " P is open by ; :: thesis: verum