( rng P c= U & dom Q = U ) by PARTFUN1:def 2;
then dom (P * Q) = dom P by RELAT_1:27
.= X by PARTFUN1:def 2 ;
hence for b₁ being X -defined Relation st b₁ = P * Q holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum