theorem Th31: :: FUNCT_4:31
for f, g being Function st dom f misses dom g holds
f \/ g = f +* g by Th30, PARTFUN1:56;