let X be non empty TopSpace; :: thesis: for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of
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,(TopSpaceMetr M) st f is continuous holds
for r being Real
for u being Element of
for P being Subset of st P = Ball u,r holds
f " P is open
let f be Function of X,(TopSpaceMetr M); :: thesis: ( f is continuous implies for r being Real
for u being Element of
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
for P being Subset of st P = Ball u,r holds
f " P is open
thus for r being Real
for u being Element of
for P being Subset of st P = Ball u,r holds
f " P is open :: thesis: verum

proof

let r be Real; :: thesis: for u being Element of
for P being Subset of st P = Ball u,r holds
f " P is open
let u be Element of ; :: 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 P' = P as Subset of ;
assume P = Ball u,r ; :: thesis: f " P is open
then ( [#] (TopSpaceMetr M) <> {} & P' is open ) by TOPMETR:21;
hence f " P is open by A1, TOPS_2:55; :: thesis: verum

end;