theorem Th2: :: GOBOARD5:2

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