theorem Th20: :: PARTFUN1:20

for x, y being object
for X being set
for f being PartFunc of X,{y} st x in dom f holds
f . x = y