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 for b₁ being A \/ B -defined Function st b₁ = f +* g holds
b₁ is total ; :: thesis: verum