dom (f1 /" f2) = C by Lm4;
hence for b₁ being PartFunc of C,RAT st b₁ = f1 /" f2 holds
b₁ is total by PARTFUN1:def 4; :: thesis: verum