theorem :: FUNCT_4:127

for z being object
for f being Function
for x, y being object st x <> y holds
(f +~ (x,y)) +~ (x,z) = f +~ (x,y)