for G being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2)
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