theorem Th45: :: PARTFUN1:45

for X, Y being set
for f being PartFunc of X,Y holds f in PFuncs (X,Y)