let X, Y 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 object ; :: 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 object such that
A1: x in dom (Y |` f) and
A2: x in X and
A3: y = (Y |` f) . x by Def6;
( y = f . x & x in dom f ) by A1, A3, Th52;
hence y in f .: X by A2, Def6; :: thesis: verum