let n be Element of NAT ; :: thesis: for q1 being Point of (TOP-REAL n) ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) & f is continuous )
let q1 be Point of (TOP-REAL n); :: thesis: ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) & f is continuous )
defpred S₁[ set , set ] means ex q being Point of (TOP-REAL n) st
( q = $1 & $2 = |.(q - q1).| );
A2: for x being set st x in the carrier of (TOP-REAL n) holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in the carrier of (TOP-REAL n) implies ex y being set st S₁[x,y] )
assume x in the carrier of (TOP-REAL n) ; :: thesis: ex y being set st S₁[x,y]
then reconsider q3 = x as Point of (TOP-REAL n) ;
take |.(q3 - q1).| ; :: thesis: S₁[x,|.(q3 - q1).|]
thus S₁[x,|.(q3 - q1).|] ; :: thesis: verum

end;

consider f1 being Function such that
A3: ( dom f1 = the carrier of (TOP-REAL n) & ( for x being set st x in the carrier of (TOP-REAL n) holds
S₁[x,f1 . x] ) ) from CLASSES1:sch 1(A2);
rng f1 c= the carrier of R^1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f1 or z in the carrier of R^1 )
assume z in rng f1 ; :: thesis: z in the carrier of R^1
then consider xz being set such that
A4: ( xz in dom f1 & z = f1 . xz ) by FUNCT_1:def 5;
consider q4 being Point of (TOP-REAL n) such that
A5: ( q4 = xz & f1 . xz = |.(q4 - q1).| ) by A3, A4;
thus z in the carrier of R^1 by A4, A5, TOPMETR:24; :: thesis: verum

end;

then reconsider f2 = f1 as Function of (TOP-REAL n),R^1 by A3, FUNCT_2:def 1, RELSET_1:11;
A6: for q being Point of (TOP-REAL n) holds f1 . q = |.(q - q1).|

proof

let q be Point of (TOP-REAL n); :: thesis: f1 . q = |.(q - q1).|
consider q2 being Point of (TOP-REAL n) such that
A7: ( q2 = q & f1 . q = |.(q2 - q1).| ) by A3;
thus f1 . q = |.(q - q1).| by A7; :: thesis: verum

end;

then f2 is continuous by Lm20;
hence ex f being Function of (TOP-REAL n),R^1 st
( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) & f is continuous ) by A6; :: thesis: verum