theorem Th19: :: PARTFUN2:19

for X being set
for C, D being non empty set
for f, g being PartFunc of C,D holds
( g = X |` f iff ( ( for c being Element of C holds
( c in dom g iff ( c in dom f & f /. c in X ) ) ) & ( for c being Element of C st c in dom g holds
g /. c = f /. c ) ) )