let x be object ; :: thesis: for X, Y being set
for f being Function st x in dom f & x in X & f . x in Y holds
<:f,X,Y:> . x = f . x
let X, Y be set ; :: thesis: for f being Function st x in dom f & x in X & f . x in Y holds
<:f,X,Y:> . x = f . x
let f be Function; :: thesis: ( x in dom f & x in X & f . x in Y implies <:f,X,Y:> . x = f . x )
assume that
A1: x in dom f and
A2: x in X and
A3: f . x in Y ; :: thesis: <:f,X,Y:> . x = f . x
x in dom (Y |` f) by A1, A3, FUNCT_1:54;
then f . x = (Y |` f) . x by FUNCT_1:55
.= ((Y |` f) | X) . x by A2, FUNCT_1:49 ;
hence <:f,X,Y:> . x = f . x ; :: thesis: verum