theorem Th4: :: BOOLMARK:4

for A being non empty set
for y being set
for f being Function holds (f +* (A --> y)) .: A = {y}