theorem :: GOBRD13:43

for k, n being Nat
for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 2 <= n & f | n turns_right k,G holds
f turns_right k,G