:: deftheorem Def3 defines PartFunc-set RFUNCT_3:def 3 :
for X, Y, b₃ being set holds
( b₃ is PartFunc-set of X,Y iff for x being Element of b₃ holds x is PartFunc of X,Y );