let k, n be Nat; :: thesis: 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

let D be set ; :: thesis: 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

let f be FinSequence of D; :: thesis: for G being Matrix of D st 1 <= k & k + 2 <= n & f | n goes_straight k,G holds
f goes_straight k,G

let G be Matrix of D; :: thesis: ( 1 <= k & k + 2 <= n & f | n goes_straight k,G implies f goes_straight k,G )
assume that
A1: ( 1 <= k & k + 2 <= n ) and
A2: f | n goes_straight k,G ; :: thesis: f goes_straight k,G
per cases ( len f <= n or n < len f ) ;
suppose len f <= n ; :: thesis: f goes_straight k,G
hence f goes_straight k,G by ; :: thesis: verum
end;
suppose A3: n < len f ; :: thesis: f goes_straight k,G
let i19, j19, i29, j29 be Nat; :: according to GOBRD13:def 8 :: thesis: ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & [i29,(j29 + 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 + 1)) ) & not ( i19 + 1 = i29 & j19 = j29 & [(i29 + 1),j29] in Indices G & f /. (k + 2) = G * ((i29 + 1),j29) ) & not ( i19 = i29 + 1 & j19 = j29 & [(i29 -' 1),j29] in Indices G & f /. (k + 2) = G * ((i29 -' 1),j29) ) implies ( i19 = i29 & j19 = j29 + 1 & [i29,(j29 -' 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 -' 1)) ) )
A4: len (f | n) = n by ;
then k + 1 in dom (f | n) by ;
then A5: (f | n) /. (k + 1) = f /. (k + 1) by FINSEQ_4:70;
k + 2 in dom (f | n) by ;
then A6: (f | n) /. (k + 2) = f /. (k + 2) by FINSEQ_4:70;
k in dom (f | n) by ;
then (f | n) /. k = f /. k by FINSEQ_4:70;
hence ( [i19,j19] in Indices G & [i29,j29] in Indices G & f /. k = G * (i19,j19) & f /. (k + 1) = G * (i29,j29) & not ( i19 = i29 & j19 + 1 = j29 & [i29,(j29 + 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 + 1)) ) & not ( i19 + 1 = i29 & j19 = j29 & [(i29 + 1),j29] in Indices G & f /. (k + 2) = G * ((i29 + 1),j29) ) & not ( i19 = i29 + 1 & j19 = j29 & [(i29 -' 1),j29] in Indices G & f /. (k + 2) = G * ((i29 -' 1),j29) ) implies ( i19 = i29 & j19 = j29 + 1 & [i29,(j29 -' 1)] in Indices G & f /. (k + 2) = G * (i29,(j29 -' 1)) ) ) by A2, A5, A6; :: thesis: verum
end;
end;