theorem :: PARTFUN2:27

for C, D being non empty set
for f being PartFunc of C,D ex g being Function of C,D st
for c being Element of C st c in dom f holds
g . c = f /. c