Edge Pairing of different Spanning Trees I've stumbled across this theorem a while ago

Let $S$ and $T$ be two Spanning Trees on the same vertex set. Then there is a bijection $F: E(S) \to E(T)$ satisfying following edge exchange property: $S - e + F(e)$ is a Spanning Tree for all $e \in E(S)$.

I find this quite interesting since it summarizes some nice properties about Spanning Trees.
I came up with a proof for this theorem, but I am not 100% sure whether the proof is actually correct. Can anyone verify its correctness? Also, if you think there is an easier way to prove it, let me know.
Proof. Let $n = | E(S)\setminus E(T) | $ be the number of edges, that differ from each Spanning Tree. We prove the theorem via induction in $n$. The case $n = 0$ is trivial since we then have $S = T.$ Now assume that we have $n+1$ edges in $S$ that are not included in $T$ and that the assumption holds for $n$. Let $e$ be any edge in $T - S$ (such an edge exists since both Spanning Trees contain equally many edges). Since $S$ is a Spanning Tree, there is a fundamental circle $C$ within $ S+ e$. Since $T$ is a Spanning Tree, we have $C \not \subseteq T$. Let $e^\prime \in C$ be any edge that is not included in T. We can now define $F(e^\prime) := e$. The condition of the statement now holds for this pair of $e$ and $e^\prime $ by construction.
Let $S^\prime := S -e^\prime + e$. Then, by the induction hypothesis, we find a bijection $G: E(S^\prime) \to E(T)$ satisfying the edge exchange property. It suffices to show, that $S - f^\prime + G(f^\prime)$ is a Spanning Tree too for all edges $f^\prime \in E(S) \cap E(S^\prime)$ (we can extend $F$ by $G$ then). Let $f^\prime \in E(S) \cap E(S^\prime)$ be such an edge and $f:= G(f^\prime)$. To see this we, we can partition the vertex set: Note that $S - e^\prime - f^\prime $ contains exactly three connected components. We label these with $S_1, S_2, S_3$ such that $e^\prime$ is a bridge between $S_1$ and $S_2$ and $f^\prime$ is a bridge between $S_2$ and $S_3$. We know that $S - e^\prime + e$ is a Spanning Tree. Therefore $e$ must be a bridge between $S_1$ and $S_2$. Since $S - e^\prime + e - f^\prime + f$ is a Spanning Tree by the inductive hypothesis, exactly one of the following cases occurs:

*

*$G(f^\prime) = f$ is a bridge between $S_1$ and $S_3$.

*$G(f^\prime) = f$ is a bridge between $S_2$ and $S_3$.

Either way, we can substitute $e^\prime$ back in for $e$ and still get a Spanning Tree. Thus, $S - f^\prime + f$ is a Spanning Tree. q.e.d.
Let me know what you think about the theorem and this proof. I think it has some nice applications, e.g. for Minimum Spanning Trees it follows that the  bijection preserves the cost function, i.e. $c(f(e)) = c(e)$ for all edges $e \in E(S)$. Also, note that the proof is highly constructive and one can easily construct an algorithm to compute the bijection. Feel free to comment if you have come up with some other applications.
 A: This is indeed a very nice result! However, there is a problem with your proof: $e$ can also go between $S_1$ and $S_3$; this would still make $S - e' + e$ a spanning tree. In this case, it is possible that $f$ goes between $S_1$ and $S_2$ and then $S - f' + f$ is not a tree. I'm skeptical as to whether this proof can be corrected, since it implies that we can choose the bijection in a "greedy manner", which seems a bit too optimistic to me.
A proof of this theorem can be found in the book Connections in Combinatorial Optimization by András Frank (it is Theorem 5.3.4 in my version of the book). It goes as follows. It is enough to find a bijection between $X = E(S) - E(T)$ and $Y = E(T) - E(S)$. Consider the bipartite graph $G'$ on $X \cup Y$ where $xy$ is an edge if and only if $x$ is in the fundamental circuit of $y$ with respect to $S$ (that is, in the unique circuit of $S + y$). Then finding a suitable bijection is equivalent to finding a perfect matching of $G'$.
We use Hall's theorem to show that there indeed is a perfect matching in $G'$. Let $Y' = \{y_1, \ldots, y_j\} \subseteq Y$ be a subset of vertices of $G'$ (note that $y_1,\ldots,y_j$ are edges of the original graph) and let $C_1, \ldots, C_j$ be the fundamental circuits of $y_1,\ldots,y_j$ with respect to $S$. Let $K = \cup_i C_i$. You can check from the definitions that the neighbour set of $Y'$ in $G'$ is $K - T$, while $Y' = K - S$. Thus we want to show $|K - T| \geq |K - S|$, or equivalently $|K \cap T| \leq |K \cap S|$. To see this, observe that $K \cap S$ is a spanning forest in the subgraph of $G$ induced by $K$: adding any edge from $K - S = Y'$ would create a cycle. On the other hand $K \cap T$ is clearly a forest in this subgraph, so it has size at most that of a spanning forest.
Note that this proof is constructive, since we can find a perfect matching of $G'$ efficiently. In the book the result is stated for matroids in general, and indeed the same proof works in the general case after we replace "spanning tree" with "basis" and "forest" with "independent set".
