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