let x, Y be set ; :: 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 4, RELAT_1:def 4;
hence ( ( x in dom f & f . x in Y ) iff [x,(f . x)] in Y | f ) by RELAT_1:def 12; :: thesis: verum