We have described the algorithm, but we don't know now whether it's correct or not. We should prove if it's correct and there are three parts of this proof, so we need to prove three things. First, we need to prove that the algorithm terminates, who knows? Maybe it will continue indefinitely and then we don't have that final matching. The second thing, at the end of the algorithm we do have a perfect matching, everybody's a pair. And the third thing is stability, that what we get is a perfect match in the end is really a stable matching. So, we need to prove three things and we will do it one by one. So let's start with termination, it's almost obvious but let me say it slowly. So let's look at every man, so when he acts he makes a new proposal. And so he moves in one direction in the list and there's no way to go back. So he can make at most n proposals because the proposal was never repeated. And we have n men, so they can make in total only n squared proposals, so there is no way to continue longer. And this is rather fast, especially if we compare this with the total number of all possible matchings. So if we have n object on the left and n object to the right. You know from the that they are n factorial possible one-to-one correspondence between them. And this is much bigger, of course. So n squared is quite practical but n factorial is infinity for practical reasons, so this is termination. Now why at the end we have a perfect matching? It's a bit more complicated, let's look at it. So imagine it's not the case, so imagine some man remains without a partner after this algorithm. This means that he made proposals to everybody in his list and each of these proposals was rejected. Either immediately rejected, or rejected after some time, so all of the women rejected him either earlier or later. So what does it mean, what does it imply? So we can conclude that all women were married at some point. Because if they rejected him, either they were married at the same time immediately, or they were married to him. So anyway, they were married at some point. And we know that for them the situation can only improve. So if they were married, they remain married later, so they remain married until the end. And then, of course, we get a contradiction because all women are married and some men are not. And we have the same number of women and men by assumption. So this is a, what is it called? The pigeonhole principle says that it's not possible, so we have a perfect matching. And the last thing is stability, it's also not very difficult, but let's look at it. So assume that it's not stable, the final, final metric is not stable. This means that there is some dangerous pair at the end of the element, let's denote this pair (m, w), so what does it mean? That for m, w is better than his current partner and for w also, but now we are looking at m. W is better than the current partner, so this better w was on the list before. Because before m proposed to his current partner he also should have proposed to w because it's early in the list. And then w rejected him, either immediately or after some time. So w rejected m at some stage, which means that at some time, her partner was better. Either when she rejected immediately or when she found a better partner than m. So at some time, w has a partner that is better than m. And then, since the things improve with time, these other later partners are also better than m. So the pair is not actually dangerous because the final partner for w is also better than m. So there is no reason for w to change. We get a contradiction with the assumption that the pair is dangerous, so this is the proof of stability. Now we have done that and we can formulate the theorem. A stable matching always exists and the proof is to use the algorithm to find it. And let's make some remarks about the theorem. So first, as we have seen, the stable matching is not unique. So our algorithm finds one of the stable matchings, not the only one. And now, it's not clear whether this matching which is found depends on the nondeterministic ordering of the actions, actually not. And we will see why later, it's a more difficult part but we will see this. And let me stress that this algorithm is extremely unfair it favors men in a very strong sense. But, of course, we can consider symmetric algorithm when women make proposals and men decide whether to accept or reject them. And, of course, this algorithm will have completely symmetric properties. So it will be unfair, also very unfair but now in the other direction.