reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;

set c = the carrier of T;

for q being Point of T ex r being Real st

( f . q = r & r >= 0 )

A1: for p being Point of T

for r1 being Real st F . p = r1 holds

H . p = sqrt r1 and

A2: H is continuous by JGRAPH_3:5;

reconsider h = H as RealMap of T by TOPMETR:17;

A3: dom h = the carrier of T by FUNCT_2:def 1

.= dom f by FUNCT_2:def 1 ;

for c being object st c in dom h holds

h . c = sqrt (f . c) by A1;

then h = sqrt f by A3, PARTFUN3:def 5;

hence for b_{1} being RealMap of T st b_{1} = sqrt f holds

b_{1} is continuous
by A2, JORDAN5A:27; :: thesis: verum

set c = the carrier of T;

for q being Point of T ex r being Real st

( f . q = r & r >= 0 )

proof

then consider H being Function of T,R^1 such that
let q be Point of T; :: thesis: ex r being Real st

( f . q = r & r >= 0 )

take f . q ; :: thesis: ( f . q = f . q & f . q >= 0 )

thus f . q = f . q ; :: thesis: f . q >= 0

dom f = the carrier of T by FUNCT_2:def 1;

then f . q in rng f by FUNCT_1:def 3;

hence f . q >= 0 by PARTFUN3:def 4; :: thesis: verum

end;( f . q = r & r >= 0 )

take f . q ; :: thesis: ( f . q = f . q & f . q >= 0 )

thus f . q = f . q ; :: thesis: f . q >= 0

dom f = the carrier of T by FUNCT_2:def 1;

then f . q in rng f by FUNCT_1:def 3;

hence f . q >= 0 by PARTFUN3:def 4; :: thesis: verum

A1: for p being Point of T

for r1 being Real st F . p = r1 holds

H . p = sqrt r1 and

A2: H is continuous by JGRAPH_3:5;

reconsider h = H as RealMap of T by TOPMETR:17;

A3: dom h = the carrier of T by FUNCT_2:def 1

.= dom f by FUNCT_2:def 1 ;

for c being object st c in dom h holds

h . c = sqrt (f . c) by A1;

then h = sqrt f by A3, PARTFUN3:def 5;

hence for b

b