:: deftheorem Def3 defines PFuncs PARTFUN1:def 3 :
for X, Y, b₃ being set holds
( b₃ = PFuncs (X,Y) iff for x being object holds
( x in b₃ iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) ) );