theorem :: FUNCT_7:114

for f being Function
for a, A, b, B, c, C being set st a <> b & a <> c holds
(((f +* (a .--> A)) +* (b .--> B)) +* (c .--> C)) . a = A