begin
theorem
:: deftheorem Def1 defines positive-yielding PARTFUN3:def 1 :
:: deftheorem Def2 defines negative-yielding PARTFUN3:def 2 :
:: deftheorem Def3 defines nonpositive-yielding PARTFUN3:def 3 :
:: deftheorem Def4 defines nonnegative-yielding PARTFUN3:def 4 :
theorem Th2:
theorem Th3:
:: deftheorem Def5 defines sqrt PARTFUN3:def 5 :