let x, X be set ; :: thesis: for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
let f be Function; :: thesis: ( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
( x in dom f iff [x,(f . x)] in f ) by FUNCT_1:def 2, RELAT_1:def 4;
hence ( ( x in dom f & x in X ) iff [x,(f . x)] in f | X ) by RELAT_1:def 11; :: thesis: verum