Propositional calculus. If there is a deduction of $t$ from $S\cup\{s\}$ in $n$ lines, ... then there is a deduction of $(s\Rightarrow t)$ in at most $3n+2$ lines. 
So I think this should be done by induction. The cases with $t$ being an axiom or a member of $S$ or $t=s$ can be proved by explicitly deducing $(s\Rightarrow t)$ in 5 lines or fewer. But what happens if $t$ is deduced from previous lines using Modus Ponens?
The axioms I am using are $$(s\Rightarrow (t \Rightarrow s)) \\((s\Rightarrow(t\Rightarrow u))\Rightarrow((s\Rightarrow t)\Rightarrow(s\Rightarrow u))) \\ (((s\Rightarrow \bot)\Rightarrow \bot)\Rightarrow s)$$
In a deduction every step is either an axiom or deduced by modus ponens.
 A: Your argument :

"If in deducing $\tau$ from $\Gamma \cup \{ \sigma \}$, $\tau$ comes by MP from previous lines $\phi$ and $\phi ⇒ \tau$ then the proof proceed as follows:

(a) write down the deduction of $\sigma ⇒ \phi$
(b) write down the deduction of $\sigma ⇒ (\phi ⇒ \tau)$ 
(c) write down $(\sigma ⇒ (\phi ⇒ \tau)) ⇒ ((\sigma ⇒ \phi) ⇒ (\sigma ⇒ \tau))$

and apply MP twice"

is sound.
Because the "upper bound" $3n+2$ is relative to the number $n$ of lines in the derivation, we have to prove it by induction on $n$.
(A) --- The induction start from the base case, i.e. $n=1$. But a one-line derivation of $\tau$ from $\Gamma \cup \{ \sigma \}$ is possible only if $\tau$ is in $\Gamma$ or it is an axiom or it is $\sigma$ itself.
If $\tau$ is in $\Gamma$ or $\tau$ is a logical axiom, we need a $3$ lines derivation :
(i) $\tau$ --- in $\Gamma$ or axiom
(ii) $\sigma ⇒ (\tau ⇒ \sigma)$ --- axiom
(iii) $\tau ⇒ \sigma$ --- by MP.
If $\tau$ is $\sigma$, we need the "standard" derivation : $\vdash \tau ⇒ \tau$, which is $5$ lines long.
Thus, in both cases, we have a resulting derivation $\le 5=3 \times n +2$, with $n=1$.
(B) --- Now we need the induction hypothesis, i.e. that $\sigma ⇒ \phi$ and $\sigma ⇒ (\phi ⇒ \tau)$ have both "resulting" derivations $\le 3 \times (n-1) +2$ lines, and we want to show that the resulting derivation for $\sigma ⇒ \tau$ has $\le 3 \times n +2$ lines. 
In the "initial" derivation we add only the line $k$-th line :

(k) $\quad \tau$ --- from previous lines $i, j$ (with $1 \le i, j, < k$) by MP,

as "justification".
Now, we have to add the axiom instance (a) above :
(l) $(\sigma ⇒ (\phi ⇒ \tau)) ⇒ ((\sigma ⇒ \phi) ⇒ (\sigma ⇒ \tau))$ --- axiom
(l+1) $(\sigma ⇒ \phi) ⇒ (\sigma ⇒ \tau)$ --- from (i) and (l) by MP
(l+2) $\sigma ⇒ \tau$ --- from (j) and (l+1) by MP.
The "resulting" derivation of $\sigma ⇒ \tau$ has $\le 3 \times (n-1) +2 +3 = 3n + 2$ lines.
