theorem Th3: :: SETWISEO:6

for X, Y being set
for f being Function holds f .: (Y \ (f " X)) = (f .: Y) \ X