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 Th16
.= C /\ (dom f2) by FUNCT_2:def 1
.= C /\ C by FUNCT_2:def 1
.= C ; :: thesis: verum