theorem Th28: :: JORDAN1H:28

for i being Nat
for G being Go-board st 1 <= i & i <= len G holds
(SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1