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]
consider t being Real such that
A2: t = dist s,x ;
reconsider t = t as Element of R^1 by TOPMETR:24;
take t ; :: thesis: S₁[s,t]
thus S₁[s,t] by A2; :: thesis: verum

end;

consider F being Function of the carrier of M,the carrier of R^1 such that
A3: for x being Element of M holds S₁[x,F . x] from FUNCT_2:sch 3(A1);
A4: for y being Point of M holds F . y = dist y,x by A3;
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 6;
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 A4; :: thesis: verum