let X, Y, x, Z be set ; :: thesis: for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds
(Z | f) . x = f . x
let f be Function of X,Y; :: thesis: ( Y <> {} & x in X & f . x in Z implies (Z | f) . x = f . x )
assume ( Y <> {} & x in X & f . x in Z ) ; :: thesis: (Z | f) . x = f . x
then ( x in dom f & f . x in Z ) by Def1;
then x in dom (Z | f) by FUNCT_1:86;
hence (Z | f) . x = f . x by FUNCT_1:87; :: thesis: verum