Does there exist a proof of closure of regular languages under regular substitution by giving the corresponding DFA?
There is a simple proof using automata. Suppose the original language is $L$, and we are substituting $R_a$ for $a$ (for each $a \in \Sigma$). Starting with an automaton for $L$, replace each edge $(x,y)$ annotated $a$ with a copy of an automaton $A_a$ for $R_a$, connecting $x$ to the starting state of $A_a$ with an $\epsilon$-edge, and connecting each accepting state of $A_a$ (which is not accepting any more in the new automaton) to $y$ with an $\epsilon$-edge.