let x, 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:86;
then f . x = (Y | f) . x by FUNCT_1:87
.= ((Y | f) | X) . x by A2, FUNCT_1:72 ;
hence <:f,X,Y:> . x = f . x ; :: thesis: verum