theorem Th15: :: PARTFUN2:15

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