let n be Element of NAT ; :: thesis: for q1 being Point of (TOP-REAL n)
for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) holds
f is continuous
let q1 be Point of (TOP-REAL n); :: thesis: for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) holds
f is continuous
let f be Function of (TOP-REAL n),R^1 ; :: thesis: ( ( for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ) implies f is continuous )
assume A1: for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ; :: thesis: f is continuous
XX: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider f1 = f as Function of (TopSpaceMetr (Euclid n)),(TopSpaceMetr RealSpace ) by TOPMETR:def 7;

now

let r be real number ; :: thesis: for u being Element of the carrier of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist u,w < s holds
dist u1,w1 < r ) )
let u be Element of the carrier of (Euclid n); :: thesis: for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist u,w < s holds
dist u1,w1 < r ) )
let u1 be Element of RealSpace ; :: thesis: ( r > 0 & u1 = f1 . u implies ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist u,w < s holds
dist u1,w1 < r ) ) )
assume A2: ( r > 0 & u1 = f1 . u ) ; :: thesis: ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist u,w < s holds
dist u1,w1 < r ) )
set s1 = r;
for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist u,w < r holds
dist u1,w1 < r

proof

let w be Element of (Euclid n); :: thesis: for w1 being Element of RealSpace st w1 = f1 . w & dist u,w < r holds
dist u1,w1 < r
let w1 be Element of RealSpace ; :: thesis: ( w1 = f1 . w & dist u,w < r implies dist u1,w1 < r )
assume A3: ( w1 = f1 . w & dist u,w < r ) ; :: thesis: dist u1,w1 < r
reconsider qw = w, qu = u as Point of (TOP-REAL n) by TOPREAL3:13;
A4: dist u,w = |.(qu - qw).| by JGRAPH_1:45;
reconsider tu = u1, tw = w1 as Real by METRIC_1:def 14;
A5: dist u1,w1 = the distance of RealSpace . u1,w1 by METRIC_1:def 1
.= abs (tu - tw) by METRIC_1:def 13, METRIC_1:def 14 ;
A6: tu = |.(qu - q1).| by A1, A2;
w1 = |.(qw - q1).| by A1, A3;
then A7: dist u1,w1 <= |.((qu - q1) - (qw - q1)).| by A5, A6, JORDAN2C:11;
|.((qu - q1) - (qw - q1)).| = |.((qu - q1) - ((- q1) + qw)).|
.= |.(((qu - q1) - (- q1)) - qw).| by EUCLID:50
.= |.(((qu + (- q1)) + q1) - qw).| by EUCLID:39
.= |.((qu + (q1 - q1)) - qw).| by EUCLID:30
.= |.((qu + (0. (TOP-REAL n))) - qw).| by EUCLID:46
.= |.(qu - qw).| by EUCLID:31 ;
hence dist u1,w1 < r by A3, A4, A7, XXREAL_0:2; :: thesis: verum

end;

hence ex s being real number st
( s > 0 & ( for w being Element of (Euclid n)
for w1 being Element of RealSpace st w1 = f1 . w & dist u,w < s holds
dist u1,w1 < r ) ) by A2; :: thesis: verum

end;

then f1 is continuous by UNIFORM1:4;
hence f is continuous by XX, PRE_TOPC:62, TOPMETR:def 7; :: thesis: verum