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