:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: PARTFUN3:1
:: 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: :: PARTFUN3:2
theorem Th3: :: PARTFUN3:3
:: deftheorem Def5 defines sqrt PARTFUN3:def 5 :