let k be Element of NAT ; :: thesis: for f being non constant standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
Int (right_cell f,k) misses L~ f
let f be non constant standard special_circular_sequence; :: thesis: ( 1 <= k & k + 1 <= len f implies Int (right_cell f,k) misses L~ f )
assume A1: ( 1 <= k & k + 1 <= len f ) ; :: thesis: Int (right_cell f,k) misses L~ f
k <= k + 1 by NAT_1:11;
then k <= len f by A1, XXREAL_0:2;
then A2: k in dom f by A1, FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A3: [i1,j1] in Indices (GoB f) and
A4: f /. k = (GoB f) * i1,j1 by GOBOARD2:25;
A5: i1 <= len (GoB f) by A3, MATRIX_1:39;
A6: j1 <= width (GoB f) by A3, MATRIX_1:39;
i1 <> 0 by A3, MATRIX_1:39;
then consider i being Nat such that
A7: i1 = i + 1 by NAT_1:6;
i <= i1 by A7, NAT_1:11;
then A8: i <= len (GoB f) by A5, XXREAL_0:2;
j1 <> 0 by A3, MATRIX_1:39;
then consider j being Nat such that
A9: j1 = j + 1 by NAT_1:6;
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 13;
A10: i1 = i + 1 by A7;
A11: j1 = j + 1 by A9;
j <= j1 by A9, NAT_1:11;
then A12: j <= width (GoB f) by A6, XXREAL_0:2;
k + 1 >= 1 by NAT_1:11;
then A13: k + 1 in dom f by A1, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A14: [i2,j2] in Indices (GoB f) and
A15: f /. (k + 1) = (GoB f) * i2,j2 by GOBOARD2:25;
A16: i2 <= len (GoB f) by A14, MATRIX_1:39;
A17: j2 <= width (GoB f) by A14, MATRIX_1:39;
reconsider i1' = i1, i2' = i2, j1' = j1, j2' = j2 as Element of REAL by XREAL_0:def 1;
(abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A3, A4, A13, A14, A15, GOBOARD5:13;
then A18: ( ( abs (i1' - i2') = 1 & j1 = j2 ) or ( abs (j1' - j2') = 1 & i1 = i2 ) ) by GOBOARD1:2;

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

suppose ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: Int (right_cell f,k) misses L~ f

then right_cell f,k = cell (GoB f),i1,j1 by A1, A3, A4, A10, A14, A15, GOBOARD5:28;
hence Int (right_cell f,k) misses L~ f by A5, A6, GOBOARD7:14; :: thesis: verum

end;

suppose ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: Int (right_cell f,k) misses L~ f

then right_cell f,k = cell (GoB f),i1,j by A1, A3, A4, A9, A14, A15, GOBOARD5:29;
hence Int (right_cell f,k) misses L~ f by A5, A12, GOBOARD7:14; :: thesis: verum

end;

suppose ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: Int (right_cell f,k) misses L~ f

then right_cell f,k = cell (GoB f),i2,j1 by A1, A3, A4, A11, A14, A15, GOBOARD5:30;
hence Int (right_cell f,k) misses L~ f by A6, A16, GOBOARD7:14; :: thesis: verum

end;

suppose ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: Int (right_cell f,k) misses L~ f

then right_cell f,k = cell (GoB f),i,j2 by A1, A3, A4, A7, A14, A15, GOBOARD5:31;
hence Int (right_cell f,k) misses L~ f by A8, A17, GOBOARD7:14; :: thesis: verum

end;

end;