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 object ; :: 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 object st
( x in dom f & x in f " Y & y = f . x ) by Def6;
hence y in Y by Def7; :: thesis: verum