let G be X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); :: thesis: for i1, i2, j1, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & (G * (i1,j1)) `1 = (G * (i2,j2)) `1 holds

i1 = i2

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,j1] in Indices G & [i2,j2] in Indices G & (G * (i1,j1)) `1 = (G * (i2,j2)) `1 implies i1 = i2 )

assume that

A1: [i1,j1] in Indices G and

A2: [i2,j2] in Indices G and

A3: (G * (i1,j1)) `1 = (G * (i2,j2)) `1 and

A4: i1 <> i2 ; :: thesis: contradiction

A5: ( 1 <= i1 & i1 <= len G ) by A1, MATRIX_0:32;

A6: ( 1 <= i2 & i2 <= len G ) by A2, MATRIX_0:32;

A7: ( 1 <= j2 & j2 <= width G ) by A2, MATRIX_0:32;

A8: ( i1 < i2 or i1 > i2 ) by A4, XXREAL_0:1;

( 1 <= j1 & j1 <= width G ) by A1, MATRIX_0:32;

then (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A5, GOBOARD5:2

.= (G * (i1,j2)) `1 by A5, A7, GOBOARD5:2 ;

hence contradiction by A3, A5, A6, A7, A8, GOBOARD5:3; :: thesis: verum

i1 = i2

let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,j1] in Indices G & [i2,j2] in Indices G & (G * (i1,j1)) `1 = (G * (i2,j2)) `1 implies i1 = i2 )

assume that

A1: [i1,j1] in Indices G and

A2: [i2,j2] in Indices G and

A3: (G * (i1,j1)) `1 = (G * (i2,j2)) `1 and

A4: i1 <> i2 ; :: thesis: contradiction

A5: ( 1 <= i1 & i1 <= len G ) by A1, MATRIX_0:32;

A6: ( 1 <= i2 & i2 <= len G ) by A2, MATRIX_0:32;

A7: ( 1 <= j2 & j2 <= width G ) by A2, MATRIX_0:32;

A8: ( i1 < i2 or i1 > i2 ) by A4, XXREAL_0:1;

( 1 <= j1 & j1 <= width G ) by A1, MATRIX_0:32;

then (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A5, GOBOARD5:2

.= (G * (i1,j2)) `1 by A5, A7, GOBOARD5:2 ;

hence contradiction by A3, A5, A6, A7, A8, GOBOARD5:3; :: thesis: verum