set B = M | A;
( dom (M | A) = (dom M) /\ A & dom M = I ) by PARTFUN1:def 2, RELAT_1:61;
then dom (M | A) = A by XBOOLE_1:28;
hence for b₁ being A -defined Function st b₁ = M | A holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum