R \/ S is total

proof

thus dom (R \/ S) = (dom R) \/ (dom S) by RELAT_1:13
.= R1 \/ (dom S) by PARTFUN1:def 4
.= R1 \/ S1 by PARTFUN1:def 4 ; :: according to PARTFUN1:def 4 :: thesis: verum

end;

hence for b₁ being Relation of (R1 \/ S1) st b₁ = R \/ S holds
b₁ is total ; :: thesis: verum