let PT be non empty TopSpace; :: thesis: for PM being MetrSpace
for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
the carrier of PM = the carrier of PT
let PM be MetrSpace; :: thesis: for f being Function of [: the carrier of PT, the carrier of PT:],REAL st f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) holds
the carrier of PM = the carrier of PT
let f be Function of [: the carrier of PT, the carrier of PT:],REAL; :: thesis: ( f is_metric_of the carrier of PT & PM = SpaceMetr ( the carrier of PT,f) implies the carrier of PM = the carrier of PT )
assume A1: f is_metric_of the carrier of PT ; :: thesis: ( not PM = SpaceMetr ( the carrier of PT,f) or the carrier of PM = the carrier of PT )
assume PM = SpaceMetr ( the carrier of PT,f) ; :: thesis: the carrier of PM = the carrier of PT
then PM = MetrStruct(# the carrier of PT,f #) by A1, PCOMPS_1:def 7;
hence the carrier of PM = the carrier of PT ; :: thesis: verum