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;

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A17, SEQM_3:41;

suppose A19: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: LSeg (f,k) c= left_cell (f,k,G)

then A20: j1 < width G by A14, NAT_1:13;
A21: (i1 -' 1) + 1 = i1 by A16, XREAL_1:235;
then i1 -' 1 < len G by A18, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,(i1 -' 1),j1) by A5, A8, A10, A19, A21, A20, GOBOARD5:18;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A19, TOPREAL1:def 3; :: thesis: verum

end;

suppose A22: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: LSeg (f,k) c= left_cell (f,k,G)

then i1 < len G by A15, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i1,j1) by A5, A8, A16, A10, A13, A22, GOBOARD5:22;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A22, TOPREAL1:def 3; :: thesis: verum

end;

suppose A23: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: LSeg (f,k) c= left_cell (f,k,G)

then A24: i2 < len G by A18, NAT_1:13;
A25: (j2 -' 1) + 1 = j2 by A12, XREAL_1:235;
then j2 -' 1 < width G by A14, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= cell (G,i2,(j2 -' 1)) by A5, A8, A9, A23, A25, A24, GOBOARD5:21;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, A11, A23, TOPREAL1:def 3; :: thesis: verum

end;

suppose A26: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: LSeg (f,k) c= left_cell (f,k,G)

then j2 < width G by A13, NAT_1:13;
then LSeg ((f /. k),(f /. (k + 1))) c= left_cell (f,k,G) by A5, A8, A16, A18, A12, A11, A26, GOBOARD5:19;
hence LSeg (f,k) c= left_cell (f,k,G) by A2, TOPREAL1:def 3; :: thesis: verum

end;

end;