theorem Th3: :: TURING_1:3

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