theorem Th2: :: TURING_1:2

for f being Function
for x, y, z, u, v being object st u <> x holds
(f +* ([x,y] .--> z)) . [u,v] = f . [u,v]