dom f = I by PARTFUN1:def 2;
then dom (f +* g) = I \/ (dom g) by Def1
.= I by XBOOLE_1:12 ;
hence for b₁ being I -defined Function st b₁ = f +* g holds
b₁ is total ; :: thesis: verum