let k be 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 that
A1: 1 <= k and
A2: 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 A2, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. k = (GoB f) * (i1,j1) by GOBOARD2:14;
A6: i1 <= len (GoB f) by A4, MATRIX_0:32;
j1 <> 0 by A4, MATRIX_0:32;
then consider j being Nat such that
A7: j1 = j + 1 by NAT_1:6;
i1 <> 0 by A4, MATRIX_0:32;
then consider i being Nat such that
A8: i1 = i + 1 by NAT_1:6;
i <= i1 by A8, NAT_1:11;
then A9: i <= len (GoB f) by A6, XXREAL_0:2;
A10: j1 <= width (GoB f) by A4, MATRIX_0:32;
k + 1 >= 1 by NAT_1:11;
then A11: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A12: [i2,j2] in Indices (GoB f) and
A13: f /. (k + 1) = (GoB f) * (i2,j2) by GOBOARD2:14;
reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def 1;
|.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A4, A5, A11, A12, A13, GOBOARD5:12;
then A14: ( ( |.(i19 - i29).| = 1 & j1 = j2 ) or ( |.(j19 - j29).| = 1 & i1 = i2 ) ) by SEQM_3:42;
reconsider i = i, j = j as Nat ;
A15: i1 = i + 1 by A8;
A16: j1 = j + 1 by A7;
A17: j2 <= width (GoB f) by A12, MATRIX_0:32;
A18: i2 <= len (GoB f) by A12, MATRIX_0:32;
j <= j1 by A7, NAT_1:11;
then A19: j <= width (GoB f) by A10, XXREAL_0: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 A14, SEQM_3:41;

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, A2, A4, A5, A15, A12, A13, GOBOARD5:27;
hence Int (right_cell (f,k)) misses L~ f by A6, A10, GOBOARD7:12; :: 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, A2, A4, A5, A7, A12, A13, GOBOARD5:28;
hence Int (right_cell (f,k)) misses L~ f by A6, A19, GOBOARD7:12; :: 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, A2, A4, A5, A16, A12, A13, GOBOARD5:29;
hence Int (right_cell (f,k)) misses L~ f by A10, A18, GOBOARD7:12; :: 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, A2, A4, A5, A8, A12, A13, GOBOARD5:30;
hence Int (right_cell (f,k)) misses L~ f by A9, A17, GOBOARD7:12; :: thesis: verum

end;

end;