ベクトルに関して とする．このとき が成立する． (証明の方針) ∀-除去 とする．このとき，の逆ベクトルは ∃-仮定 である．いま，に対して 平行移動 を行う．他方，に関しての倍は であり と置き，ここで とすれば である．そして∃-導入，∃-除去を適用すれば…