let f be Function; for x, y, z, u, v being object st u <> x holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
let x, y, z, u, v be object ; ( u <> x implies (f +* ([x,y] .--> z)) . [u,v] = f . [u,v] )
set p = [x,y] .--> z;
assume
u <> x
; (f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
then A1:
[u,v] <> [x,y]
by XTUPLE_0:1;
not [u,v] in dom ([x,y] .--> z)
by A1, TARSKI:def 1;
hence
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
by FUNCT_4:11; verum