theorem Th1: :: GOBOARD5:1

for i, j being Nat
for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * (i,j)) `2 = (G * (1,j)) `2