let Y, X be set ; :: thesis: for f being Function holds (Y | f) .: X c= f .: X
let f be Function; :: thesis: (Y | f) .: X c= f .: X
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (Y | f) .: X or y in f .: X )
assume y in (Y | f) .: X ; :: thesis: y in f .: X
then consider x being set such that
A1: x in dom (Y | f) and
A2: x in X and
A3: y = (Y | f) . x by Def12;
( y = f . x & x in dom f ) by A1, A3, Th85;
hence y in f .: X by A2, Def12; :: thesis: verum