そもそも>>696の定理、関数解析の本に普通に載っている。

Liner operators Part 1: General Theory,
Nelson Dunford, Jacob T. Schwartz

の421ページ目の Lemma10 が>>696と同じもの。
証明も>>729と似たようなもの。
もちろん、有限次元だろうが無限次元だろうか関係なく成立し、
Kの標数も無制限。