for f, g being Function st dom f misses dom g holds
for A being set holds (f +* g) " A = (f " A) \/ (g " A) by Th1, PARTFUN1:56;