let Y be set ; :: thesis: for f being Function holds f .: (f " Y) = Y /\ (f .: (dom f))
let f be Function; :: thesis: f .: (f " Y) = Y /\ (f .: (dom f))
( f .: (f " Y) c= Y & f .: (f " Y) c= f .: (dom f) ) by Th145, RELAT_1:114;
hence f .: (f " Y) c= Y /\ (f .: (dom f)) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: Y /\ (f .: (dom f)) c= f .: (f " Y)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y /\ (f .: (dom f)) or y in f .: (f " Y) )
assume A1: y in Y /\ (f .: (dom f)) ; :: thesis: y in f .: (f " Y)
then y in f .: (dom f) by XBOOLE_0:def 4;
then consider x being set such that
A2: x in dom f and
x in dom f and
A3: y = f . x by Def12;
y in Y by A1, XBOOLE_0:def 4;
then x in f " Y by A2, A3, Def13;
hence y in f .: (f " Y) by A2, A3, Def12; :: thesis: verum