let f be Function; :: thesis: 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 ; :: thesis: ( u <> x implies (f +* ([x,y] .--> z)) . [u,v] = f . [u,v] )
set p = [x,y] .--> z;
assume u <> x ; :: thesis: (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; :: thesis: verum