for K, L, x, y being set
for f being Function holds (f +* (L --> y)) .: K c= (f .: K) \/ {y}