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 goes_straight k,G holds
f goes_straight k,G