dom (R \/ S) = (dom R) \/ (dom S) by XTUPLE_0:23
.= R1 \/ (dom S) by PARTFUN1:def 2
.= R1 \/ S1 by PARTFUN1:def 2 ;
hence for b₁ being Relation of (R1 \/ S1) st b₁ = R \/ S holds
b₁ is total ; :: thesis: verum