let n be 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 ) )
consider h being Function of (TOP-REAL n),R^1 such that
A1: for q being Point of (TOP-REAL n) holds h . q = |.q.| and
A2: h is continuous by Th68;
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).|
reconsider q = g . t as Point of (TOP-REAL n) ;
dom g = the carrier of I[01] by FUNCT_2:def 1;
then (h * g) . t = h . (g . t) by FUNCT_1:13
.= |.q.| by A1 ;
hence (h * g) . t = |.(g . t).| ; :: thesis: verum

end;

assume 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 )
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 A2, A3; :: thesis: verum