theorem Th32: :: GOBRD11:32

for i, j being Nat
for G being empty-yielding X_equal-in-line Y_equal-in-column Matrix of (TOP-REAL 2) st 1 <= i & i < len G & 1 <= j & j < width G holds
cell (G,i,j) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s & s <= (G * (1,(j + 1))) `2 ) }