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