theorem Th11:
for
i1,
i2,
j1,
j2 being
Nat for
G1,
G2 being
Go-board st
Values G1 c= Values G2 &
[i1,j1] in Indices G1 &
[i2,j2] in Indices G2 &
G1 * (
i1,
j1)
= G2 * (
i2,
j2) holds
cell (
G2,
(i2 -' 1),
j2)
c= cell (
G1,
(i1 -' 1),
j1)