let f1, f2 be complex-valued Function; :: thesis: dom (f1 /" f2) = (dom f1) /\ (dom f2)
thus dom (f1 /" f2) = (dom f1) /\ (dom (f2 ")) by Def4
.= (dom f1) /\ (dom f2) by Def7 ; :: thesis: verum