defpred S₁[ Element of M, Element of R^1] means for s being Element of M
for t being Element of R^1 st $1 = s & $2 = t holds
t = dist (s,x);
A1: for s being Element of M ex t being Element of R^1 st S₁[s,t]

proof

let s be Element of M; :: thesis: ex t being Element of R^1 st S₁[s,t]
dist (s,x) in REAL by XREAL_0:def 1;
then reconsider t = dist (s,x) as Element of R^1 by TOPMETR:17;
take t ; :: thesis: S₁[s,t]
thus S₁[s,t] ; :: thesis: verum

end;

consider F being Function of the carrier of M, the carrier of R^1 such that
A2: for x being Element of M holds S₁[x,F . x] from FUNCT_2:sch 3(A1);
A3: for y being Point of M holds F . y = dist (y,x) by A2;
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;
then reconsider F = F as Function of (TopSpaceMetr M),R^1 ;
take F ; :: thesis: for y being Point of M holds F . y = dist (y,x)
thus for y being Point of M holds F . y = dist (y,x) by A3; :: thesis: verum