theorem Th3: :: GOBRD13:10

for i1, j1, j2 being Nat
for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * ((len G2),j2) holds
i1 = len G1