theorem Th72: :: PARTFUN1:72

for X, Y being set
for f being PartFunc of X,Y holds
( f is total iff TotFuncs f = {f} )