let X, Y, Z be set ; :: thesis: for x being object
for f being Function of X,Y st Y <> {} & x in X & f . x in Z holds
(Z |` f) . x = f . x
let x be object ; :: 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:54;
hence (Z |` f) . x = f . x by FUNCT_1:55; :: thesis: verum