let G be Y_equal-in-column Y_increasing-in-line 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)) `2 = (G * (i2,j2)) `2 holds
j1 = j2
let i1, i2, j1, j2 be Nat; :: thesis: ( [i1,j1] in Indices G & [i2,j2] in Indices G & (G * (i1,j1)) `2 = (G * (i2,j2)) `2 implies j1 = j2 )
assume that
A1: [i1,j1] in Indices G and
A2: [i2,j2] in Indices G and
A3: (G * (i1,j1)) `2 = (G * (i2,j2)) `2 and
A4: j1 <> j2 ; :: thesis: contradiction
A5: ( 1 <= j1 & j1 <= width G ) by A1, MATRIX_0:32;
A6: ( j1 < j2 or j1 > j2 ) by A4, XXREAL_0:1;
A7: ( 1 <= i2 & i2 <= len G ) by A2, MATRIX_0:32;
A8: ( 1 <= j2 & j2 <= width G ) by A2, MATRIX_0:32;
A9: ( 1 <= i1 & i1 <= len G ) by A1, MATRIX_0:32;
then (G * (i1,j2)) `2 = (G * (1,j2)) `2 by A8, GOBOARD5:1
.= (G * (i2,j2)) `2 by A7, A8, GOBOARD5:1 ;
hence contradiction by A3, A9, A5, A8, A6, GOBOARD5:4; :: thesis: verum