let Y1, Y2 be set ; :: thesis: for f being Function holds f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)
let f be Function; :: thesis: f " (Y1 \ Y2) = (f " Y1) \ (f " Y2)
for x being object holds
( x in f " (Y1 \ Y2) iff x in (f " Y1) \ (f " Y2) )

proof

let x be object ; :: thesis: ( x in f " (Y1 \ Y2) iff x in (f " Y1) \ (f " Y2) )
A1: ( x in f " Y2 iff ( f . x in Y2 & x in dom f ) ) by Def7;
A2: ( x in f " (Y1 \ Y2) iff ( f . x in Y1 \ Y2 & x in dom f ) ) by Def7;
( x in f " Y1 iff ( f . x in Y1 & x in dom f ) ) by Def7;
hence ( x in f " (Y1 \ Y2) iff x in (f " Y1) \ (f " Y2) ) by A1, A2, XBOOLE_0:def 5; :: thesis: verum

end;

hence f " (Y1 \ Y2) = (f " Y1) \ (f " Y2) by TARSKI:2; :: thesis: verum