Prove that \(I {\ \land \ }B \to {wp\left(V_1 := V; S, V < V_1\right)}\).
\[\begin{split} & {wp\left(V_1 := V; S, V < V_1\right)}\\ {\ ({\mathbf{§2}})} \iff & {wp\left(V_{1} := n - i + 1, {wp\left(res := res * i, {wp\left(i := i + 1, n - i + 1 \lt V_{1}\right)}\right)}\right)} \\ {\ ({\mathbf{§1}})} \iff & {wp\left(V_{1} := n - i + 1, {wp\left(res := res * i, n - i \lt V_{1}\right)}\right)} \\ {\ ({\mathbf{§1}})} \iff & {wp\left(V_{1} := n - i + 1, n - i\lt V_{1}\right)} \\ {\ ({\mathbf{§1}})} \iff & n - i \lt n - i + 1 \\ \end{split}\]
This is trivially true, meaning that
\[\begin{split} & I {\ \land \ }B \to (n - i \lt n - i + 1) \end{split}\]
always will be true.