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 set ; :: 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 set such that
A1: x in dom f and
A2: x in X /\ (f " Y) and
A3: y = f . x by Def12;
( x in X & x in f " Y ) by A2, XBOOLE_0:def 4;
then ( y in f .: X & y in Y ) by A1, A3, Def12, Def13;
hence y in (f .: X) /\ Y by XBOOLE_0:def 4; :: thesis: verum