begin
theorem
:: deftheorem Def1 defines positive-yielding PARTFUN3:def 1 :
for R being Relation holds
( R is positive-yielding iff for r being real number st r in rng R holds
0 < r );
:: deftheorem Def2 defines negative-yielding PARTFUN3:def 2 :
for R being Relation holds
( R is negative-yielding iff for r being real number st r in rng R holds
0 > r );
:: deftheorem Def3 defines nonpositive-yielding PARTFUN3:def 3 :
for R being Relation holds
( R is nonpositive-yielding iff for r being real number st r in rng R holds
0 >= r );
:: deftheorem Def4 defines nonnegative-yielding PARTFUN3:def 4 :
for R being Relation holds
( R is nonnegative-yielding iff for r being real number st r in rng R holds
0 <= r );
theorem Th2:
theorem Th3:
:: deftheorem Def5 defines sqrt PARTFUN3:def 5 :
for f being real-valued Function
for b2 being Function holds
( b2 = sqrt f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 . x = sqrt (f . x) ) ) );