theorem Th70: :: PARTFUN1:70

for X, Y being set
for f, g being PartFunc of X,Y st g in TotFuncs f holds
g is total