let F1, F2 be Function of (TopSpaceMetr M),R^1 ; :: thesis: ( ( for y being Point of M holds F1 . y = dist y,x ) & ( for y being Point of M holds F2 . y = dist y,x ) implies F1 = F2 )
assume A5: for y being Point of M holds F1 . y = dist y,x ; :: thesis: ( ex y being Point of M st not F2 . y = dist y,x or F1 = F2 )
assume A6: for y being Point of M holds F2 . y = dist y,x ; :: thesis: F1 = F2
F1 = F2

proof

for y being set st y in the carrier of (TopSpaceMetr M) holds
F1 . y = F2 . y

proof

let y be set ; :: thesis: ( y in the carrier of (TopSpaceMetr M) implies F1 . y = F2 . y )
assume A7: y in the carrier of (TopSpaceMetr M) ; :: thesis: F1 . y = F2 . y
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 6;
then reconsider y = y as Point of M by A7;
F1 . y = dist y,x by A5
.= F2 . y by A6 ;
hence F1 . y = F2 . y ; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:18; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum