let Y be set ; :: thesis: for f being Function holds f .: (f " Y) c= Y
let f be Function; :: thesis: f .: (f " Y) c= Y
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (f " Y) or y in Y )
assume y in f .: (f " Y) ; :: thesis: y in Y
then ex x being set st
( x in dom f & x in f " Y & y = f . x ) by Def12;
hence y in Y by Def13; :: thesis: verum