theorem Th1: :: TOPGEN_5:1

for f, g being Function st f tolerates g holds
for A being set holds (f +* g) " A = (f " A) \/ (g " A)