theorem Th39: :: PARTFUN2:39

for X being set
for C, D being non empty set
for f being PartFunc of C,D st X misses dom f holds
f | X is constant