theorem Th2: :: CQC_SIM1:2

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