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 = upper_bound ((dist s) .: P);
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]
set t = upper_bound ((dist s) .: P);
upper_bound ((dist s) .: P) in REAL by XREAL_0:def 1;
then reconsider t = upper_bound ((dist s) .: P) 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 = upper_bound ((dist y) .: P) 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 x being Point of M holds F . x = upper_bound ((dist x) .: P)
thus for x being Point of M holds F . x = upper_bound ((dist x) .: P) by A3; :: thesis: verum