Exactly.

No, for the reality proof, you have the double assumption. For the orthogonality proof, you ONLY assume that the eigenvalues differ. Since eigenkets are, by definition, nonzero, proving orthogonality (which follows only from the Hermitian nature of the operator and the differing eigenvalues) will, in effect, prove that the eigenkets are not equal. But you'reSo for orthonormality we also take the double assumption but in the sense the eigen values AND eigenkets are NOT equalprovingthat. Assume as little as you need to, and prove as much as you can!

ie

are orthonormal

Cheers :-)