dom (f1 - f2) = C by Lm3;
hence f1 - f2 is total PartFunc of C, COMPLEX by PARTFUN1:def 4; :: thesis: verum