let i1, j1, i2, j2 be Nat; :: thesis: for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds
( i1 = i2 & j1 = j2 )
let G be Go-board; :: thesis: ( [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) implies ( i1 = i2 & j1 = j2 ) )
assume that
A1: [i1,j1] in Indices G and
A2: [i2,j2] in Indices G and
A3: G * (i1,j1) = G * (i2,j2) ; :: thesis: ( i1 = i2 & j1 = j2 )
A4: 1 <= i1 by A1, MATRIX_0:32;
A5: j1 <= width G by A1, MATRIX_0:32;
A6: 1 <= j1 by A1, MATRIX_0:32;
A7: 1 <= i2 by A2, MATRIX_0:32;
A8: i1 <= len G by A1, MATRIX_0:32;
A9: i2 <= len G by A2, MATRIX_0:32;
A10: j2 <= width G by A2, MATRIX_0:32;
A11: 1 <= j2 by A2, MATRIX_0:32;
then A12: (G * (i1,j2)) `2 = (G * (1,j2)) `2 by A4, A8, A10, GOBOARD5:1
.= (G * (i1,j1)) `2 by A3, A7, A9, A11, A10, GOBOARD5:1 ;
A13: (G * (i1,j2)) `1 = (G * (i1,1)) `1 by A4, A8, A11, A10, GOBOARD5:2
.= (G * (i1,j1)) `1 by A4, A8, A6, A5, GOBOARD5:2 ;
assume A14: ( not i1 = i2 or not j1 = j2 ) ; :: thesis: contradiction
per cases ( i1 < i2 or i1 > i2 or j1 < j2 or j1 > j2 ) by A14, XXREAL_0:1;
suppose i1 < i2 ; :: thesis: contradiction
hence contradiction by A3, A4, A9, A11, A10, A13, GOBOARD5:3; :: thesis: verum
end;
suppose i1 > i2 ; :: thesis: contradiction
hence contradiction by A3, A8, A7, A11, A10, A13, GOBOARD5:3; :: thesis: verum
end;
suppose j1 < j2 ; :: thesis: contradiction
hence contradiction by A4, A8, A6, A10, A12, GOBOARD5:4; :: thesis: verum
end;
suppose j1 > j2 ; :: thesis: contradiction
hence contradiction by A4, A8, A5, A11, A12, GOBOARD5:4; :: thesis: verum
end;
end;