let n be 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 6;
assume A2: for q being Point of (TOP-REAL n) holds f . q = |.q.| ; :: 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)
.= |.(tu - tw).| by METRIC_1:def 12 ;
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, Th3, JGRAPH_1:28;
hence dist (u1,w1) < r by A6, 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