let x be object ; :: according to VALUED_0:def 9 :: thesis: ( not x in dom (sqrt f) or not (sqrt f) . x is real )
set F = sqrt f;
assume x in dom (sqrt f) ; :: thesis: (sqrt f) . x is real
then (sqrt f) . x = sqrt (f . x) by Def5;
hence (sqrt f) . x is real ; :: thesis: verum