theorem Th4: :: PARTFUN1:4

for x being object
for Y being set
for f being b₂ -valued Function st x in dom f holds
f . x in Y