per cases by A10;

suppose A15: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis:

take cell ((GoB f),i1,j1) ; :: thesis:
let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A16: [i19,j19] in Indices (GoB f) and
A17: [i29,j29] in Indices (GoB f) and
A18: f /. k = (GoB f) * (i19,j19) and
A19: f /. (k + 1) = (GoB f) * (i29,j29) ; :: thesis:
A20: i1 = i19 by A4, A5, A16, A18, GOBOARD1:5;
j1 = j19 by A4, A5, A16, A18, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,j1) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,j1) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A15, A17, A19, A20, GOBOARD1:5; :: thesis:

end;

suppose A21: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis:

take cell ((GoB f),i1,(j1 -' 1)) ; :: thesis:
let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A22: [i19,j19] in Indices (GoB f) and
A23: [i29,j29] in Indices (GoB f) and
A24: f /. k = (GoB f) * (i19,j19) and
A25: f /. (k + 1) = (GoB f) * (i29,j29) ; :: thesis:
A26: i1 = i19 by A4, A5, A22, A24, GOBOARD1:5;
j1 = j19 by A4, A5, A22, A24, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i1,(j1 -' 1)) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A21, A23, A25, A26, GOBOARD1:5; :: thesis:

end;

suppose A27: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis:

take cell ((GoB f),i2,j2) ; :: thesis:
let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A28: [i19,j19] in Indices (GoB f) and
A29: [i29,j29] in Indices (GoB f) and
A30: f /. k = (GoB f) * (i19,j19) and
A31: f /. (k + 1) = (GoB f) * (i29,j29) ; :: thesis:
A32: i2 = i29 by A7, A8, A29, A31, GOBOARD1:5;
j1 = j19 by A4, A5, A28, A30, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),i2,j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),i2,j2) = cell ((GoB f),(i19 -' 1),j29) ) ) by A4, A5, A7, A8, A27, A28, A29, A30, A31, A32, GOBOARD1:5; :: thesis:

end;

suppose A33: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:

take cell ((GoB f),(i1 -' 1),j2) ; :: thesis:
let i19, j19, i29, j29 be Nat; :: thesis:
assume that
A34: [i19,j19] in Indices (GoB f) and
A35: [i29,j29] in Indices (GoB f) and
A36: f /. k = (GoB f) * (i19,j19) and
A37: f /. (k + 1) = (GoB f) * (i29,j29) ; :: thesis:
A38: i1 = i19 by A4, A5, A34, A36, GOBOARD1:5;
j1 = j19 by A4, A5, A34, A36, GOBOARD1:5;
hence ( ( i19 = i29 & j19 + 1 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,j19) ) or ( i19 + 1 = i29 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i19,(j19 -' 1)) ) or ( i19 = i29 + 1 & j19 = j29 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),i29,j29) ) or ( i19 = i29 & j19 = j29 + 1 & cell ((GoB f),(i1 -' 1),j2) = cell ((GoB f),(i19 -' 1),j29) ) ) by A7, A8, A33, A35, A37, A38, GOBOARD1:5; :: thesis:

end;

end;