set IT = R | X;
dom R = Y by PARTFUN1:def 2;
then A1: dom (R | X) = X null Y by RELAT_1:61;
reconsider ITT = R | X as X -defined Relation ;
thus for b₁ being X -defined Relation st b₁ = R | X holds
b₁ is total by A1, PARTFUN1:def 2; :: thesis: verum