let f be Function; :: thesis: for x, y, z, u, v being set st v <> y holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]
let x, y, z, u, v be set ; :: 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 ZFMISC_1:33;
dom ([x,y] .--> z) = {[x,y]} by FUNCOP_1:19;
then 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:12; :: thesis: verum