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