theorem Th29: :: JORDAN1H:29

for j being Nat
for G being Go-board st 1 <= j & j <= width G holds
(SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2