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 Th74, 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 object ; :: 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 object such that
A2: x in dom f and
x in dom f and
A3: y = f . x by Def6;
y in Y by A1, XBOOLE_0:def 4;
then x in f " Y by A2, A3, Def7;
hence y in f .: (f " Y) by A2, A3, Def6; :: thesis: verum