let x be object ; 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 ; 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; ( 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
; <: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
; verum