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 ^2 ) & 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 ^2 ) & 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 ^2 ) & 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 * r1 and
A2: g1 is continuous by JGRAPH_2:22;
for p being Point of X
for r1 being Real st f1 . p = r1 holds
g1 . p = r1 ^2 by A1;
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 ^2 ) & g is continuous ) by A2; :: thesis: verum