let Y be set ; :: thesis: for x being object
for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
let x be object ; :: thesis: for f being Function holds
( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
let f be Function; :: thesis: ( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f )
( x in dom f iff [x,(f . x)] in f ) by FUNCT_1:def 2, XTUPLE_0:def 12;
hence ( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y |` f ) by RELAT_1:def 12; :: thesis: verum