A1: dom g = B by PARTFUN1:def 2;
dom f = A by PARTFUN1:def 2;
then dom (f +* g) = A \/ B by A1, FUNCT_4:def 1;
hence f +* g is A \/ B -defined by RELAT_1:def 18; :: thesis: verum