dom (R ~) = rng R by RELAT_1:20
.= Y by FUNCT_2:def 3 ;
hence for b₁ being Y -defined Relation st b₁ = R ~ holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum