let G be Go-board; :: thesis: 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; :: thesis: ( f is_sequence_on G implies Values (GoB f) c= Values G )
assume A1: f is_sequence_on G ; :: thesis: Values (GoB f) c= Values G
set F = GoB f;
let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in Values (GoB f) or p in Values G )
assume p in Values (GoB f) ; :: thesis: p in Values G
then p in { ((GoB f) * i,j) where i, j is Element of NAT : [i,j] in Indices (GoB f) } by Th7;
then consider i, j being Element of NAT such that
A2: p = (GoB f) * i,j and
A3: [i,j] in Indices (GoB f) ;
A4: ( 1 <= i & i <= len (GoB f) & 1 <= j & j <= width (GoB f) ) by A3, MATRIX_1:39;
reconsider p = p as Point of (TOP-REAL 2) by A2;
consider k1 being Element of NAT such that
A5: k1 in dom f and
A6: p `1 = (f /. k1) `1 by A2, A4, Lm2;
consider k2 being Element of NAT such that
A7: k2 in dom f and
A8: p `2 = (f /. k2) `2 by A2, A4, Lm3;
consider i1, j1 being Element of NAT such that
A9: [i1,j1] in Indices G and
A10: f /. k1 = G * i1,j1 by A1, A5, GOBOARD1:def 11;
A11: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G ) by A9, MATRIX_1:39;
consider i2, j2 being Element of NAT such that
A12: [i2,j2] in Indices G and
A13: f /. k2 = G * i2,j2 by A1, A7, GOBOARD1:def 11;
A14: ( 1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G ) by A12, MATRIX_1:39;
then A15: (G * i1,j2) `1 = (G * i1,1) `1 by A11, GOBOARD5:3
.= (G * i1,j1) `1 by A11, GOBOARD5:3 ;
A16: (G * i1,j2) `2 = (G * 1,j2) `2 by A11, A14, GOBOARD5:2
.= (G * i2,j2) `2 by A14, GOBOARD5:2 ;
A17: [i1,j2] in Indices G by A11, A14, MATRIX_1:37;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
then p = G * i1,j2 by A6, A8, A10, A13, A15, A16, EUCLID:57;
then p in { (G * k,l) where k, l is Element of NAT : [k,l] in Indices G } by A17;
hence p in Values G by Th7; :: thesis: verum