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