theorem :: GRFUNC_1:13

for f, g being Function st dom f misses dom g holds
f \/ g is Function