theorem :: FUNCOP_1:69

for F, f, g being Function st [:(rng f),(rng g):] c= dom F holds
dom (F .: (f,g)) = (dom f) /\ (dom g)