To prove this, properness makes . First rule out : a sequence with eventually lies in a fixed sublevel set, which is bounded by coercivity. A -convergent subsequence would then have a limit with , contradicting the codomain. Hence is finite.
Choose a minimizing sequence with . It eventually belongs to the bounded sublevel set . Extract . By sequential lower semicontinuity,
Thus . In particular, a reflexive Banach space with the weak topology supplies the required subsequence property by weak sequential compactness of bounded sequences in a reflexive Banach space. A strictly convex function has at most one minimizer; this is an additional property, not part of the existence theorem.