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

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