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 )
proof
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;
then consider H being Function of T,R^1 such that
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 b1 being RealMap of T st b1 = sqrt f holds
b1 is continuous by A2, JORDAN5A:27; :: thesis: verum