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 8;
hence the carrier of PM = the carrier of PT ; :: thesis: verum