theorem Th31: :: FUNCT_7:32

for f being Function
for d, i, j being object st i <> j holds
(f +* (i,d)) . j = f . j