theorem Th12:
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,
(j2 -' 1))
c= cell (
G1,
i1,
(j1 -' 1))