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