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