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