thus dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def3
.= C /\ (dom f2) by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C ; :: according to PARTFUN1:def 2 :: thesis: verum