theorem :: FUNCT_4:91

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