We define a relation R such that , where a choice function C is defined as such that is an element of . Since and is not empty, the existence of choice function C is followed from a Form1, satisfying the Form 2.
Conversely, assume Form 2.
Let ; let .
Now, we have and for each i, .
That means, there exists a choice function such that we retrieve for each .
Now, consider any relation R. The existence of a choice function C provides us with a mapping from to .
Then, , i.e., . Thus, .