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:71;
hence dom (F .: f,g) = dom <:f,g:> by A1, RELAT_1:46, XBOOLE_1:1
.= (dom f) /\ (dom g) by FUNCT_3:def 8 ;
:: thesis: verum