let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G)
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G) )
assume A1: f is_sequence_on G ; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg (f,k) c= left_cell (f,k,G)
let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies LSeg (f,k) c= left_cell (f,k,G) )
assume A2: ( 1 <= k & k + 1 <= len f ) ; :: thesis: LSeg (f,k) c= left_cell (f,k,G)
then A3: k in dom f by SEQ_4:134;
then consider i1, j1 being Nat such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * (i1,j1) by A1, GOBOARD1:def 9;
A6: k + 1 in dom f by A2, SEQ_4:134;
then consider i2, j2 being Nat such that
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * (i2,j2) by A1, GOBOARD1:def 9;
A9: 1 <= i2 by A7, MATRIX_0:32;
A10: 1 <= j1 by A4, MATRIX_0:32;
left_cell (f,k,G) = left_cell (f,k,G) ;
then A11: ( ( i1 = i2 & j1 + 1 = j2 & left_cell (f,k,G) = cell (G,(i1 -' 1),j1) ) or ( i1 + 1 = i2 & j1 = j2 & left_cell (f,k,G) = cell (G,i1,j1) ) or ( i1 = i2 + 1 & j1 = j2 & left_cell (f,k,G) = cell (G,i2,(j2 -' 1)) ) or ( i1 = i2 & j1 = j2 + 1 & left_cell (f,k,G) = cell (G,i1,j2) ) ) by A1, A2, A4, A5, A7, A8, GOBRD13:def 3;
A12: 1 <= j2 by A7, MATRIX_0:32;
A13: j1 <= width G by A4, MATRIX_0:32;
A14: j2 <= width G by A7, MATRIX_0:32;
A15: i2 <= len G by A7, MATRIX_0:32;
A16: 1 <= i1 by A4, MATRIX_0:32;
|.(i1 - i2).| + |.(j1 - j2).| = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def 9;
then A17: ( ( |.(i1 - i2).| = 1 & j1 = j2 ) or ( |.(j1 - j2).| = 1 & i1 = i2 ) ) by SEQM_3:42;
A18: i1 <= len G by A4, MATRIX_0:32;