theorem :: BVFUNC14:12

for f being Function
for C, D, c, d being object st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c by Lm1;