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
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in Values (GoB f) or p in Values G )
set F = GoB f;
assume p in Values (GoB f) ; :: thesis: 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; :: thesis: verum