let C be set ; :: thesis: for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
let D1, D2 be non empty complex-membered set ; :: thesis: for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
let f1 be Function of C,D1; :: thesis: for f2 being Function of C,D2 holds dom (f1 - f2) = C
let f2 be Function of C,D2; :: thesis: dom (f1 - f2) = C
thus dom (f1 - f2) = (dom f1) /\ (dom (- f2)) by Def1
.= C /\ (dom (- f2)) by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C ; :: thesis: verum