theorem Th89: :: FUNCT_4:89

for f being Function
for a, b, n, m being object holds ((f +* (a .--> b)) +* (m .--> n)) . m = n