theorem Th15: :: MESFUN13:1

for X being set
for A being Subset of X
for f being b₁ -defined Relation holds f | (A `) = f | ((dom f) \ A)