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