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 M

for P being Subset of (TopSpaceMetr M) 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 M

for P being Subset of (TopSpaceMetr M) 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 M

for P being Subset of (TopSpaceMetr M) 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 (TopSpaceMetr M) 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 (TopSpaceMetr M) st P = Ball (u,r) holds

f " P is open

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

f " P is open

let P be Subset of (TopSpaceMetr M); :: thesis: ( P = Ball (u,r) implies f " P is open )

reconsider P9 = P as Subset of (TopSpaceMetr M) ;

assume P = Ball (u,r) ; :: thesis: f " P is open

then ( [#] (TopSpaceMetr M) <> {} & P9 is open ) by TOPMETR:14;

hence f " P is open by A1, TOPS_2:43; :: thesis: verum

for f being Function of X,(TopSpaceMetr M) st f is continuous holds

for r being Real

for u being Element of M

for P being Subset of (TopSpaceMetr M) 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 M

for P being Subset of (TopSpaceMetr M) 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 M

for P being Subset of (TopSpaceMetr M) 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 (TopSpaceMetr M) 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 (TopSpaceMetr M) st P = Ball (u,r) holds

f " P is open

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

f " P is open

let P be Subset of (TopSpaceMetr M); :: thesis: ( P = Ball (u,r) implies f " P is open )

reconsider P9 = P as Subset of (TopSpaceMetr M) ;

assume P = Ball (u,r) ; :: thesis: f " P is open

then ( [#] (TopSpaceMetr M) <> {} & P9 is open ) by TOPMETR:14;

hence f " P is open by A1, TOPS_2:43; :: thesis: verum