let X, Y be set ; :: thesis: for f being Function holds f .: (Y \ (f " X)) = (f .: Y) \ X
let f be Function; :: thesis: f .: (Y \ (f " X)) = (f .: Y) \ X
now :: thesis: for x being object holds
( ( x in f .: (Y \ (f " X)) implies x in (f .: Y) \ X ) & ( x in (f .: Y) \ X implies x in f .: (Y \ (f " X)) ) )
let x be object ; :: thesis: ( ( x in f .: (Y \ (f " X)) implies x in (f .: Y) \ X ) & ( x in (f .: Y) \ X implies x in f .: (Y \ (f " X)) ) )
thus ( x in f .: (Y \ (f " X)) implies x in (f .: Y) \ X ) :: thesis: ( x in (f .: Y) \ X implies x in f .: (Y \ (f " X)) )
proof
assume x in f .: (Y \ (f " X)) ; :: thesis: x in (f .: Y) \ X
then consider z being object such that
A1: z in dom f and
A2: z in Y \ (f " X) and
A3: f . z = x by FUNCT_1:def 6;
not z in f " X by A2, XBOOLE_0:def 5;
then A4: not x in X by A1, A3, FUNCT_1:def 7;
f . z in f .: Y by A1, A2, FUNCT_1:def 6;
hence x in (f .: Y) \ X by A3, A4, XBOOLE_0:def 5; :: thesis: verum
end;
assume A5: x in (f .: Y) \ X ; :: thesis: x in f .: (Y \ (f " X))
then consider z being object such that
A6: z in dom f and
A7: z in Y and
A8: f . z = x by FUNCT_1:def 6;
not x in X by A5, XBOOLE_0:def 5;
then not z in f " X by A8, FUNCT_1:def 7;
then z in Y \ (f " X) by A7, XBOOLE_0:def 5;
hence x in f .: (Y \ (f " X)) by A6, A8, FUNCT_1:def 6; :: thesis: verum
end;
hence f .: (Y \ (f " X)) = (f .: Y) \ X by TARSKI:2; :: thesis: verum