We are proving that \(I {\ \land \ }B \to {wp\left(S, I\right)}\)
\[\begin{split} & I {\ \land \ }B &\to& {wp\left(S, I\right)}\\ & I {\ \land \ }B &\to& {wp\left(res := res * i; i := i + 1, I\right)}\\ {\ ({\mathbf{§2}})} \iff & I {\ \land \ }B &\to& {wp\left(res := res * i, {wp\left(i := i + 1, I\right)}\right)}\\ {\ ({\mathbf{§1}})} \iff & I {\ \land \ }B &\to& {wp\left(res := res * i, (i + 1 \leq n + 1) {\ \land \ }(res = i!)\right)}\\ {\ ({\mathbf{§1}})} \iff & I {\ \land \ }B &\to& (i + 1 \leq n + 1) {\ \land \ }(res * i = i!)\\ \end{split}\]
Substituting \(I, B\) we get:
\[\begin{split} \iff & (i \leq n + 1) {\ \land \ }(res = (i - 1)!) {\ \land \ }(i \leq n) & \to\\ & (i + 1 \leq n + 1) {\ \land \ }(res * i = i!) &\\ \iff & {{\mathbf{\top}}}& \end{split}\]
This holds true since: \[\begin{cases} i \leq n &\iff& i + 1 \leq n + 1\\ res = (i - 1)! &\iff& res * i = i! \end{cases}\]