let G be X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2); :: thesis: for i1, i2, j1, j2 being Element of 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 Element of 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_1:39;
A6: ( 1 <= i2 & i2 <= len G ) by A2, MATRIX_1:39;
A7: ( 1 <= j2 & j2 <= width G ) by A2, MATRIX_1:39;
A8: ( i1 < i2 or i1 > i2 ) by A4, XXREAL_0:1;
( 1 <= j1 & j1 <= width G ) by A1, MATRIX_1:39;
then (G * i1,j1) `1 = (G * i1,1) `1 by A5, GOBOARD5:3
.= (G * i1,j2) `1 by A5, A7, GOBOARD5:3 ;
hence contradiction by A3, A5, A6, A7, A8, GOBOARD5:4; :: thesis: verum