defpred S_{1}[ 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_{1}[s,t]

A2: for x being Element of M holds S_{1}[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

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

proof

consider F being Function of the carrier of M, the carrier of R^1 such that
let s be Element of M; :: thesis: ex t being Element of R^1 st S_{1}[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_{1}[s,t]

thus S_{1}[s,t]
; :: thesis: verum

end;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

thus S

A2: for x being Element of M holds S

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