:: deftheorem Def5 defines TotFuncs PARTFUN1:def 5 :
for X, Y being set
for f being PartFunc of X,Y
for b₄ being set holds
( b₄ = TotFuncs f iff for x being object holds
( x in b₄ iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) );