let n be Element of NAT ; :: thesis: for g being Function of I[01] ,(TOP-REAL n) st g is continuous holds
ex f being Function of I[01] ,R^1 st
( ( for t being Point of I[01] holds f . t = |.(g . t).| ) & f is continuous )
let g be Function of I[01] ,(TOP-REAL n); :: thesis: ( g is continuous implies ex f being Function of I[01] ,R^1 st
( ( for t being Point of I[01] holds f . t = |.(g . t).| ) & f is continuous ) )
assume A1: g is continuous ; :: thesis: ex f being Function of I[01] ,R^1 st
( ( for t being Point of I[01] holds f . t = |.(g . t).| ) & f is continuous )
consider h being Function of (TOP-REAL n),R^1 such that
A2: ( ( for q being Point of (TOP-REAL n) holds h . q = |.q.| ) & h is continuous ) by Th92;
set f1 = h * g;
A3: for t being Point of I[01] holds (h * g) . t = |.(g . t).|

proof

let t be Point of I[01] ; :: thesis: (h * g) . t = |.(g . t).|
A4: dom g = the carrier of I[01] by FUNCT_2:def 1;
reconsider q = g . t as Point of (TOP-REAL n) ;
(h * g) . t = h . (g . t) by A4, FUNCT_1:23
.= |.q.| by A2 ;
hence (h * g) . t = |.(g . t).| ; :: thesis: verum

end;

h * g is continuous by A1, A2;
hence ex f being Function of I[01] ,R^1 st
( ( for t being Point of I[01] holds f . t = |.(g . t).| ) & f is continuous ) by A3; :: thesis: verum