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