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

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