let n be Element of NAT ; :: thesis: for f being Function of (TOP-REAL n),R^1 st ( for q being Point of (TOP-REAL n) holds f . q = |.q.| ) 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.| ) 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 7;
assume A2: for q being Point of (TOP-REAL n) holds f . q = |.q.| ; :: thesis: f is continuous

now

let r be real number ; :: 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 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 (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 that
A3: r > 0 and
A4: 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 that
A5: w1 = f1 . w and
A6: dist u,w < r ; :: thesis: dist u1,w1 < r
reconsider tu = u1, tw = w1 as Real by METRIC_1:def 14;
reconsider qw = w, qu = u as Point of (TOP-REAL n) by TOPREAL3:13;
A7: 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 ;
A8: tu = |.qu.| by A2, A4;
w1 = |.qw.| by A2, A5;
then ( dist u,w = |.(qu - qw).| & dist u1,w1 <= |.(qu - qw).| ) by A7, A8, Th11, JGRAPH_1:45;
hence dist u1,w1 < r by A6, 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 A3; :: thesis: verum

end;

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