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 that
A1: ( Y <> {} & x in X ) and
A2: f . x in Z ; :: thesis: (Z | f) . x = f . x
x in dom f by A1, Def1;
then x in dom (Z | f) by A2, FUNCT_1:86;
hence (Z | f) . x = f . x by FUNCT_1:87; :: thesis: verum