虽然标题用了证明这个词，但是实际上只是对核心部分的一个说明，并不是完整的证明。完整的证明比较繁琐，请大家自行看Tarjan的原论文/各种算法书籍（其实是我又菜又懒得看）。

y总讲的时候没有讲证明，本咸鱼狗尾续貂一下，满足一下和我一样的有强迫症的同学。

前置知识

1. 深度优先搜索；
2. 有向图的联通性；
3. 强连通分量的定义；
4. Tarjan算法是什么。

对于以上前置知识，这里不会做解释。

Tarjan算法模板

这里以y总的模板为例。

// N 表示点数，M 表示边数
int h[N], e[M], ne[M], cnt; // 存储有向图, h[]需要初始化成-1
int belong[N], stap[N], stop, instack[N], dfn[N], low[N], bent, dindex ;
// bent存储强联通分量的个数，belong[i] 存储第i个点处于哪个强联通分量中

void add (int a, int b)
{
    e[cnt] = b ; ne[cnt] = h[a] ; h[a] = cnt ++ ;
}

void tarjan (int i)
{
    dfn[i] = low[i] = ++ dindex ;
    instack[stap[ ++ stop] = i] = 1 ;
    for (int p = h[i]; p != -1; p = ne[p])
    {
        int j = e[p] ;
        if (!dfn[j])
        {
            tarjan (j) ;
            if (low[j] < low[i]) low[i] = low[j] ;
        }
        else if (instack[j] && dfn[j] < low[i]) low[i] = dfn[j] ;
    }

    if (dfn[i] == low[i])
    {
        ++ bent ;
        int j;
        do
        {
            j = stap[stop -- ] ;
            instack[j] = 0 ;
            belong[j] = bent ;

        } while (j != i) ;
    }
}

作者：yxc
链接：https://www.acwing.com/blog/content/42/
来源：AcWing
著作权归作者所有。商业转载请联系作者获得授权，非商业转载请注明出处。

下文会用的到的词汇和符号说明

i: 当前所在的点；
dfn[i]: i的搜索顺序（时间戳）；
low[i]: 从i出发，可以到的时间戳最小的点；

问题

说明一个问题之前，我们需要定义清楚问题。
这里的核心问题是：
为什么当dfn[i] == low[i]的时候，通过将i以及栈中i以上（假设栈顶在上面）的元素全部出栈，可以恰好找到i所在的强连通分量的全部元素。

正文说明

首先我们需要注意到，算法在执行到什么时候出栈。
根据上面的模板，我们是在从i点出发的深度优先搜索结束，回溯到i点的时候，如果此刻dfn[i] == low[i]，才会开始出栈。

接下来，根据此时此刻图中所有点和栈和i的关系，我们可以把点分成这么几类。

1. i自己；
2. 不在栈中且没进过栈的点；
3. 不在栈中但是已经出栈了的点；
4. 在栈中且在i上面的点；
5. 在栈中且在i下面的点。

容易发现这个分类是不重不漏的，接下来会对每类点进行说明。

1.i自己。

略

2.不在栈中且没进过栈的点。

注意到此刻我们已经完成了从点i出发的DFS，并且回溯到了i点，所以所有从i出发能到的点，我们都见过了，在模板的第二行，如果见过这个点，那么它是必然进过栈的。所以这些点，是从i出发没办法到达的点，因此它们不在i所在的强连通分量中。

3.不在栈中但是已经出栈了的点。

记这个点是y好了。这里有两种可能。

第一种可能：y在见到i之前见到。因为已经出栈了，所以是不可能从y出发到达i的。因为如果从y出发可以到达i的话，此时此刻，y应该停留在栈中才对。

第二种可能：y在见到i之后见到。此时从i出发是可以到达y的。假设y能到达的最早节点是x。那么这个x要么是比i更早见到的，要么是比i更晚见到的。如果x是比i更早见到的，那么low[i] <= dfn[x]才行，这与low[i] == dfn[i]矛盾了。
如果x是比i更晚见到的，那么说明从y出发没办法到达i，所以此时y不属于i所在的强连通分量。

4.在栈中且在i上面的点。

因为此刻是从i出发的DFS结束，回溯到i，所以从i出发是可以到比i晚进栈且此时在栈中的节点的。那么从这些点（记为z）出发，可以到达i吗？是可以的。假设从z出发到达不了i。那么有两种情形，第一种是到到达比i更早的节点，和3中的情况类似，此时low[i] < dfn[i]，矛盾了。第二种是到达比i更晚的节点，记最早的那个为w。那么在回溯的过程中，回溯到w的时候，z此刻会出栈。所以在回溯到i的时候，它已经不在栈中了，矛盾了。因此从z出发一定可以回到i。

5.在栈中且在i下面的点。

如果从i出发能到这些点的话，那么low[i] < dfn[i]，与假设矛盾了。

综上所述，第一类和第四类的点构成了i所在的强连通分量。

参考

https://blog.csdn.net/KEYboarderQQ/article/details/71308102
我在原文基础上补充了更多细节。