theorem :: FUNCT_1:69

for Y1, Y2 being set
for f being Function holds f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)