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 )
A1: 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 6;
assume A2: for q being Point of (TOP-REAL n) holds f . q = |.(q - q1).| ; :: thesis: f is continuous

now :: thesis: for r being Real
for u being Element of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real 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 r be Real; :: thesis: for u being Element of (Euclid n)
for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real 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 (Euclid n); :: thesis: for u1 being Element of RealSpace st r > 0 & u1 = f1 . u holds
ex s being Real 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 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 that
A3: r > 0 and
A4: u1 = f1 . u ; :: thesis: ex s being Real 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 that
A5: w1 = f1 . w and
A6: dist (u,w) < r ; :: thesis: dist (u1,w1) < r
reconsider tu = u1, tw = w1 as Real ;
reconsider qw = w, qu = u as Point of (TOP-REAL n) by TOPREAL3:8;
A7: dist (u1,w1) = the distance of RealSpace . (u1,w1) by METRIC_1:def 1
.= |.(tu - tw).| by METRIC_1:def 12, METRIC_1:def 13 ;
A8: tu = |.(qu - q1).| by A2, A4;
A9: |.((qu - q1) - (qw - q1)).| = |.((qu - q1) - ((- q1) + qw)).|
.= |.(((qu - q1) - (- q1)) - qw).| by RLVECT_1:27
.= |.(((qu + (- q1)) + q1) - qw).|
.= |.((qu + (q1 - q1)) - qw).| by RLVECT_1:def 3
.= |.((qu + (0. (TOP-REAL n))) - qw).| by RLVECT_1:5
.= |.(qu - qw).| by RLVECT_1:4 ;
w1 = |.(qw - q1).| by A2, A5;
then ( dist (u,w) = |.(qu - qw).| & dist (u1,w1) <= |.((qu - q1) - (qw - q1)).| ) by A7, A8, JGRAPH_1:28, JORDAN2C:9;
hence dist (u1,w1) < r by A6, A9, XXREAL_0:2; :: thesis: verum

end;

hence ex s being Real 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 A3; :: thesis: verum

end;

then f1 is continuous by UNIFORM1:3;
hence f is continuous by A1, PRE_TOPC:32, TOPMETR:def 6; :: thesis: verum