Updating an MST $T$ when the weight of an edge not in $T$ is decreased
Let $T$ be a minimum spanning tree of $G$. Let $e$ be the edge we modify to get $G'$, and let $T'$ be the tree computed according to the algorithm. We know that weight of $T'$ is less than or equal to the weight of $T$.

Firstly, $T'$ is a tree - we create exactly one cycle in the algorithm, and break it, so we have no cycles in $T'$.

Secondly $T'$ is a spanning tree of $G'$. Let $e'$ be the edge removed and $e''$ be the edge added in the algorithm (we have either $e'' = e'$ or $e'' = e$) . To be a spanning tree, we must have a path between every pair of vertices $u$, $v$ using only edges of $T'$. Suppose that in $T$ (which is definitely a spanning tree), the path from $u$ to $v$ did not involve $e'$, then the same path exists in $T'$. Alternatively, suppose that it did use $e'$, then there is a path (without loss of generality) from $u$ to one endpoint of $e'$ and from the other endpoint of $e'$ to $v$. There is also a path from one endpoint of $e'$ to the other endpoint via $e''$ (around the cycle), all within $T'$. Then we can construct a path from $u$ to $v$ via $e''$ in $T'$ by merging these three paths and removing the overlap (although a walk is sufficient for connectivity).

Now, the important part, we wish to prove that $T'$ is a minimum spanning tree for $G'$.

Case 1: The algorithm does not add $e$ to the tree. In this case $T' = T$. Suppose that there is a minimum spanning tree $H$ for $G'$ that is different to $T'$. If $H$ has the same weight as $T'$, we're done. Now suppose for contradiction that the weight of $H$ is less than the weight of $T'$. There must be some edge $e'$ of lowest weight that is in $H$ but not in $T'$ (there must be some edge that does better, otherwise $G$ would not be of lower weight than $T'$, moreover we can assume that the edge that does better is the lowest weight edge that's not in $T'$ - we can take any $H'$ that is a lower weight tree than $T'$ and look at the candidate for $e'$, if it is not smaller than any edge in its cycle, then either $H'$ is not an MST, or we can create a new $H'$ where we swap the $e'$ for some edge of $T'$, this process must terminate with an edge $e'$ which has the property that it is the edge that does better).


If $e' \neq e$, then consider the tree obtained by adding $e'$ to $T$ (note, not $T'$), and removing the highest weight edge on the cycle formed. This new tree has weight less than that of $T$ and is a spanning tree for $G$, contradicting the fact that $T$ is an MST for $G$ - so we know this can't happen.
If $e' = e$, consider the cycle formed by adding $e' = e$ to $T'$ (i.e. the one the algorithm considered). All other edges in the cycle have lower weight than $e'$ (otherwise the algorithm would've included $e$ as an edge), and hence must be in $H$ (as $e'$ is the lowest weight edge that is not already in $T'$), but then $H$ must contain a cycle, so isn't a tree and we have a contradiction.


Case 2: The algorithm adds $e$ to $T'$. Let $x$ be the edge in $T$ that is removed by the algorithm (and hence not in $T'$) Again assume we have another MST $H$ as before. If the weight is the same, we're happy. So assume for contradiction that $H$ has lower weight, and as before $e'$ is the lowest weight edge in $H$ that's not in $T'$. We can make similar arguments as before with $x$.


If $e' \neq x$, (note also that $e' \neq e$), then we can improve $T$ as before, but we know that $T$ is an MST, and recalling the property that we can assume $e'$ has lower weight that at least one edge in the cycle its addition induces, this gives a contradiction and $H$ can't exist.
If $e' = x$, then again $e'$ must have higher weight than all the other edges in the cycle, hence $H$ must contain all these edges and $H$ is not a tree, and we derive a contradiction.


So in every case we derive a contradiction, therefore there can be no spanning tree of lower weight that $T'$, hence $T'$ is a minimum spanning tree for $G'$.