In How were these SDE derived? I don't understand one part of Gordon's answer, specifically:
$$\ln S_t=\ln F_{0,t}-\frac{\sigma^2}{4\lambda}(1-e^{-2\lambda t})+\sigma e^{-\lambda t}\int_0^t e^{\lambda s}dB_s$$ $$d\ln S_t=\bigg(\frac{\partial \ln F_{0,t}}{\partial t}-\frac{\sigma^2 }{2}e^{-2\lambda t}-\lambda \sigma e^{-\lambda t}\int_0^t e^{\lambda s}dB_s\bigg)dt+\sigma dB_t$$
My question is, how to get from the first line to the second. Evidently, Ito's Lemma was applied, however it has been used in a way in which I have not encountered. It seems that the integral with the Brownian motion term was treated as a constant, but I don't see how that is allowed when there is $t$ in the upper limit.
Any help is appreciated.
Edit: I have come up with a solution, as long as the following is valid. Can anyone please confirm? The first line uses the product rule. \begin{align} d\bigg(\sigma e^{-\lambda t}\int_0^t e^{-\lambda s}dB_s\bigg)&=d(\sigma e^{-\lambda t})\int_0^t e^{-\lambda s}dB_s+\sigma e^{-\lambda t}d\bigg(\int_0^t e^{\lambda s}dB_s\bigg)\\ &=-\lambda\sigma e^{-\lambda t}dt \int_0^t e^{-\lambda s}dB_s+\sigma e^{-\lambda t}e^{\lambda t}dB_t\\ &=-\lambda\sigma e^{-\lambda t}dt \int_0^t e^{-\lambda s}dB_s+\sigma dB_t \end{align}