let X be set ; :: thesis: for x being object
for f being Function holds
( ( x in dom f & x in X ) iff [x,(f . x)] in f | X )
let x be object ; :: 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, XTUPLE_0:def 12;
hence ( ( x in dom f & x in X ) iff [x,(f . x)] in f | X ) by RELAT_1:def 11; :: thesis: verum