( dom f1 = C & dom f2 = C ) by FUNCT_2:def 1;
then dom (f1 + f2) = C /\ C by Def1
.= C ;
hence for b₁ being PartFunc of C,NAT st b₁ = f1 + f2 holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum