for f being Function
for X, y, z being set holds (f +* (X --> y)) +* (X --> z) = f +* (X --> z)