let X be non empty TopSpace; :: thesis: for f1 being Function of X,R^1 st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = |.r1.| ) & g is continuous )
let f1 be Function of X,R^1; :: thesis: ( f1 is continuous implies ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = |.r1.| ) & g is continuous ) )
assume f1 is continuous ; :: thesis: ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = |.r1.| ) & g is continuous )
then consider g1 being Function of X,R^1 such that
A1: for p being Point of X
for r1 being Real st f1 . p = r1 holds
g1 . p = r1 ^2 and
A2: g1 is continuous by Th6;
for q being Point of X ex r being Real st
( g1 . q = r & r >= 0 )
proof
let q be Point of X; :: thesis: ex r being Real st
( g1 . q = r & r >= 0 )
reconsider r11 = f1 . q as Real ;
g1 . q = r11 ^2 by A1;
hence ex r being Real st
( g1 . q = r & r >= 0 ) by XREAL_1:63; :: thesis: verum
end;
then consider g2 being Function of X,R^1 such that
A3: for p being Point of X
for r1 being Real st g1 . p = r1 holds
g2 . p = sqrt r1 and
A4: g2 is continuous by A2, JGRAPH_3:5;
for p being Point of X
for r1 being Real st f1 . p = r1 holds
g2 . p = |.r1.|
proof
let p be Point of X; :: thesis: for r1 being Real st f1 . p = r1 holds
g2 . p = |.r1.|
let r1 be Real; :: thesis: ( f1 . p = r1 implies g2 . p = |.r1.| )
assume f1 . p = r1 ; :: thesis: g2 . p = |.r1.|
then g1 . p = r1 ^2 by A1;
then g2 . p = sqrt (r1 ^2) by A3
.= |.r1.| by COMPLEX1:72 ;
hence g2 . p = |.r1.| ; :: thesis: verum
end;
hence ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being Real st f1 . p = r1 holds
g . p = |.r1.| ) & g is continuous ) by A4; :: thesis: verum