let G be Go-board; for f being standard special_circular_sequence st f is_sequence_on G holds
Values (GoB f) c= Values G
let f be standard special_circular_sequence; ( f is_sequence_on G implies Values (GoB f) c= Values G )
assume A1:
f is_sequence_on G
; Values (GoB f) c= Values G
let p be object ; TARSKI:def 3 ( not p in Values (GoB f) or p in Values G )
set F = GoB f;
assume
p in Values (GoB f)
; p in Values G
then
p in { ((GoB f) * (i,j)) where i, j is Nat : [i,j] in Indices (GoB f) }
by MATRIX_0:39;
then consider i, j being Nat such that
A2:
p = (GoB f) * (i,j)
and
A3:
[i,j] in Indices (GoB f)
;
reconsider p = p as Point of (TOP-REAL 2) by A2;
A4:
( 1 <= j & j <= width (GoB f) )
by A3, MATRIX_0:32;
A5:
( 1 <= i & i <= len (GoB f) )
by A3, MATRIX_0:32;
then consider k1 being Nat such that
A6:
k1 in dom f
and
A7:
p `1 = (f /. k1) `1
by A2, A4, Lm1;
consider k2 being Nat such that
A8:
k2 in dom f
and
A9:
p `2 = (f /. k2) `2
by A2, A5, A4, Lm2;
consider i2, j2 being Nat such that
A10:
[i2,j2] in Indices G
and
A11:
f /. k2 = G * (i2,j2)
by A1, A8, GOBOARD1:def 9;
A12:
( 1 <= i2 & i2 <= len G )
by A10, MATRIX_0:32;
consider i1, j1 being Nat such that
A13:
[i1,j1] in Indices G
and
A14:
f /. k1 = G * (i1,j1)
by A1, A6, GOBOARD1:def 9;
A15:
( 1 <= j1 & j1 <= width G )
by A13, MATRIX_0:32;
A16:
p = |[(p `1),(p `2)]|
by EUCLID:53;
A17:
( 1 <= j2 & j2 <= width G )
by A10, MATRIX_0:32;
A18:
( 1 <= i1 & i1 <= len G )
by A13, MATRIX_0:32;
then A19:
[i1,j2] in Indices G
by A17, MATRIX_0:30;
A20: (G * (i1,j2)) `2 =
(G * (1,j2)) `2
by A18, A17, GOBOARD5:1
.=
(G * (i2,j2)) `2
by A12, A17, GOBOARD5:1
;
(G * (i1,j2)) `1 =
(G * (i1,1)) `1
by A18, A17, GOBOARD5:2
.=
(G * (i1,j1)) `1
by A18, A15, GOBOARD5:2
;
then
p = G * (i1,j2)
by A7, A9, A14, A11, A20, A16, EUCLID:53;
then
p in { (G * (k,l)) where k, l is Nat : [k,l] in Indices G }
by A19;
hence
p in Values G
by MATRIX_0:39; verum