for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for x being Point of T holds dist (pmet,x) is continuous