let X, Y be set ; :: thesis: for f being Function holds f .: (X /\ (f " Y)) = (f .: X) /\ Y
let f be Function; :: thesis: f .: (X /\ (f " Y)) = (f .: X) /\ Y
thus f .: (X /\ (f " Y)) c= (f .: X) /\ Y by Th78; :: according to XBOOLE_0:def 10 :: thesis: (f .: X) /\ Y c= f .: (X /\ (f " Y))
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (f .: X) /\ Y or y in f .: (X /\ (f " Y)) )
assume A1: y in (f .: X) /\ Y ; :: thesis: y in f .: (X /\ (f " Y))
then y in f .: X by XBOOLE_0:def 4;
then consider x being object such that
A2: x in dom f and
A3: x in X and
A4: y = f . x by Def6;
y in Y by A1, XBOOLE_0:def 4;
then x in f " Y by A2, A4, Def7;
then x in X /\ (f " Y) by A3, XBOOLE_0:def 4;
hence y in f .: (X /\ (f " Y)) by A2, A4, Def6; :: thesis: verum