dom (f1 - f2) = C by Lm3;
hence for b₁ being PartFunc of C,REAL st b₁ = f1 - f2 holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum