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 )
assume A1: for q being Point of (TOP-REAL n) holds f . q = |.q.| ; :: thesis: f is continuous
V: 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.| by A1, A2;
w1 = |.qw.| by A1, A3;
then dist u1,w1 <= |.(qu - qw).| by A5, A6, Th11;
hence dist u1,w1 < r by A3, A4, 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 TOPMETR:def 7, UNIFORM1:4;
hence f is continuous by V, PRE_TOPC:62, TOPMETR:def 7; :: thesis: verum