let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for k being Element of 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 Element of 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 Element of NAT st 1 <= k & k + 1 <= len f holds
LSeg f,k c= left_cell f,k,G
let k be Element of 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 GOBOARD2:3;
then consider i1, j1 being Element of NAT such that
A4: [i1,j1] in Indices G and
A5: f /. k = G * i1,j1 by A1, GOBOARD1:def 11;
A6: k + 1 in dom f by A2, GOBOARD2:3;
then consider i2, j2 being Element of NAT such that
A7: [i2,j2] in Indices G and
A8: f /. (k + 1) = G * i2,j2 by A1, GOBOARD1:def 11;
A9: 1 <= i2 by A7, MATRIX_1:39;
A10: 1 <= j1 by A4, MATRIX_1:39;
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_1:39;
A13: j1 <= width G by A4, MATRIX_1:39;
A14: j2 <= width G by A7, MATRIX_1:39;
A15: i2 <= len G by A7, MATRIX_1:39;
A16: 1 <= i1 by A4, MATRIX_1:39;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A1, A3, A6, A4, A5, A7, A8, GOBOARD1:def 11;
then A17: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by GOBOARD1:2;
A18: i1 <= len G by A4, MATRIX_1:39;

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, GOBOARD1:1;

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:237;
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:19;
hence LSeg f,k c= left_cell f,k,G by A2, A11, A19, TOPREAL1:def 5; :: 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:23;
hence LSeg f,k c= left_cell f,k,G by A2, A11, A22, TOPREAL1:def 5; :: 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:237;
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:22;
hence LSeg f,k c= left_cell f,k,G by A2, A11, A23, TOPREAL1:def 5; :: 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:20;
hence LSeg f,k c= left_cell f,k,G by A2, TOPREAL1:def 5; :: thesis: verum

end;

end;