let F, f, g be Function; :: thesis: ( [:(rng f),(rng g):] c= dom F implies dom (F .: (f,g)) = (dom f) /\ (dom g) )
assume A1: [:(rng f),(rng g):] c= dom F ; :: thesis: dom (F .: (f,g)) = (dom f) /\ (dom g)
rng <:f,g:> c= [:(rng f),(rng g):] by FUNCT_3:51;
hence dom (F .: (f,g)) = dom <:f,g:> by A1, RELAT_1:27, XBOOLE_1:1
.= (dom f) /\ (dom g) by FUNCT_3:def 7 ;
:: thesis: verum