Lemma 9.3.
F
(
π
r
O
K
)
F
(
π
r
+
1
O
K
)
≅
(
k
,
+
)
for all
r
≥
1
.