Strategic form representation of extensive form games Proposition. Every finite extensive form game is associated with a unique strategic form representation.


I think this proposition is true. But how do we prove it rigorously?
I rely on the definitions from Chapter 2 of the Handbook of Game Theory, Volume 1, by Sergiu Hart.

If I understand you correctly, the proposition can be re-written as

Proposition. For, every finite extensive form game $\Gamma^E$, there exists a single
 strategic form representation $\Gamma^N =[I^N,\{S^N_i\},\{u^N_i(\cdot)\}]$ (up to relabeling of the agents) such that


$I^N = I^E$,


and for all $i\in I^N = I^E$,


$S^N_i = \{$ pure strategies of $i$ in $\Gamma^E$ $\}$ ,
and $u^N_i(s) = u^E_i(c(s))$, where $c(s) $ associates every profile of pure strategy in $\Gamma^E$  with a terminal node of  $\Gamma^E$ resulting from the pure strategy profile $s$.


I think 1. and 2. are obvious. There only remains to show 3, which is equivalent to proving that $c(s)$ is a function, i.e. every profile of pure strategies is associated with one and only one terminal node in $\Gamma^E$. This follows directly from the fact that the pure strategy of some player $i$ is a function selecting one and only one possible action from every information set. 


Start from the root node, $r_0$. 
By definition of a game in extensive form, the nodes are partitioned between the agents.
Thus $r_0$ belongs to some agent $i_0$.
By definition of the game in extensive form, the nodes of $i_0$ are partitioned into information sets.
Thus $r_0$ belongs to some information set of $i_0$, say $H_i^0$.
By definition of the pure strategy $s$, for any node in  $H_i^0$, $i_0$ always choses a single successor, among the possible successors at $H_i^0$.
Let this successor be $r_1$.
Then $r_1$ must be the successor of $r_0$, and the next node on the path.
Now consider $r_1$.
By definition of agame in extensive form, the nodes are partitioned between the agents.
Thus $r_1$ belong to some agent $i_1$ (where $i_1 = i_0$ is allowed).
$\vdots$
Repeating the argument as many time as needed, because the game is finite, we necessarily reach a single terminal node $r_* = c(s)$.