let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G implies for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f )
assume A1: f is_sequence_on G ; :: thesis: for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f
let i, j be Nat; :: thesis: ( 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f implies G * (i,j) in rng f )
assume that
A2: 1 <= i and
A3: i <= len G and
A4: 1 <= j and
A5: j <= width G ; :: thesis: ( not G * (i,j) in L~ f or G * (i,j) in rng f )
assume G * (i,j) in L~ f ; :: thesis: G * (i,j) in rng f
then consider k being Nat such that
A6: 1 <= k and
A7: k + 1 <= len f and
A8: G * (i,j) in LSeg ((f /. k),(f /. (k + 1))) by SPPOL_2:14;
consider i1, j1, i2, j2 being Nat such that
A9: [i1,j1] in Indices G and
A10: f /. k = G * (i1,j1) and
A11: [i2,j2] in Indices G and
A12: f /. (k + 1) = G * (i2,j2) and
A13: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A6, A7, JORDAN8:3;
A14: 1 <= i1 by A9, MATRIX_0:32;
A15: 1 <= j2 by A11, MATRIX_0:32;
A16: i2 <= len G by A11, MATRIX_0:32;
k + 1 >= 1 by NAT_1:11;
then A17: k + 1 in dom f by A7, FINSEQ_3:25;
A18: 1 <= j1 by A9, MATRIX_0:32;
k < len f by A7, NAT_1:13;
then A19: k in dom f by A6, FINSEQ_3:25;
A20: i1 <= len G by A9, MATRIX_0:32;
A21: j2 <= width G by A11, MATRIX_0:32;
A22: 1 <= i2 by A11, MATRIX_0:32;
A23: j1 <= width G by A9, MATRIX_0:32;