let n, i be Nat; :: thesis: for G being Go-board

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds

for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1

let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds

for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1

let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) implies for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 )

assume that

A1: f is_sequence_on G and

A2: i in dom f and

A3: i + 1 in dom f and

A4: ( n in dom G & f /. i in rng (Line (G,n)) ) ; :: thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 )

consider j1, j2 being Nat such that

A5: [j1,j2] in Indices G and

A6: f /. (i + 1) = G * (j1,j2) by A1, A3;

A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;

then A8: j1 in dom G by A5, ZFMISC_1:87;

consider i1, i2 being Nat such that

A9: [i1,i2] in Indices G and

A10: f /. i = G * (i1,i2) by A1, A2;

A11: i2 in Seg (width G) by A9, A7, ZFMISC_1:87;

len (Line (G,i1)) = width G by MATRIX_0:def 7;

then A12: i2 in dom (Line (G,i1)) by A11, FINSEQ_1:def 3;

(Line (G,i1)) . i2 = f /. i by A10, A11, MATRIX_0:def 7;

then A13: f /. i in rng (Line (G,i1)) by A12, FUNCT_1:def 3;

i1 in dom G by A9, A7, ZFMISC_1:87;

then i1 = n by A4, A13, Th2;

then A14: |.(n - j1).| + |.(i2 - j2).| = 1 by A1, A2, A3, A9, A10, A5, A6;

A15: j2 in Seg (width G) by A5, A7, ZFMISC_1:87;

len (Line (G,j1)) = width G by MATRIX_0:def 7;

then A16: j2 in dom (Line (G,j1)) by A15, FINSEQ_1:def 3;

A17: (Line (G,j1)) . j2 = f /. (i + 1) by A6, A15, MATRIX_0:def 7;

then A18: f /. (i + 1) in rng (Line (G,j1)) by A16, FUNCT_1:def 3;

|.(n - k).| = 1 ) ; :: thesis: verum

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds

for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1

let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) holds

for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1

let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & i in dom f & i + 1 in dom f & n in dom G & f /. i in rng (Line (G,n)) & not f /. (i + 1) in rng (Line (G,n)) implies for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 )

assume that

A1: f is_sequence_on G and

A2: i in dom f and

A3: i + 1 in dom f and

A4: ( n in dom G & f /. i in rng (Line (G,n)) ) ; :: thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 )

consider j1, j2 being Nat such that

A5: [j1,j2] in Indices G and

A6: f /. (i + 1) = G * (j1,j2) by A1, A3;

A7: Indices G = [:(dom G),(Seg (width G)):] by MATRIX_0:def 4;

then A8: j1 in dom G by A5, ZFMISC_1:87;

consider i1, i2 being Nat such that

A9: [i1,i2] in Indices G and

A10: f /. i = G * (i1,i2) by A1, A2;

A11: i2 in Seg (width G) by A9, A7, ZFMISC_1:87;

len (Line (G,i1)) = width G by MATRIX_0:def 7;

then A12: i2 in dom (Line (G,i1)) by A11, FINSEQ_1:def 3;

(Line (G,i1)) . i2 = f /. i by A10, A11, MATRIX_0:def 7;

then A13: f /. i in rng (Line (G,i1)) by A12, FUNCT_1:def 3;

i1 in dom G by A9, A7, ZFMISC_1:87;

then i1 = n by A4, A13, Th2;

then A14: |.(n - j1).| + |.(i2 - j2).| = 1 by A1, A2, A3, A9, A10, A5, A6;

A15: j2 in Seg (width G) by A5, A7, ZFMISC_1:87;

len (Line (G,j1)) = width G by MATRIX_0:def 7;

then A16: j2 in dom (Line (G,j1)) by A15, FINSEQ_1:def 3;

A17: (Line (G,j1)) . j2 = f /. (i + 1) by A6, A15, MATRIX_0:def 7;

then A18: f /. (i + 1) in rng (Line (G,j1)) by A16, FUNCT_1:def 3;

now :: thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 )end;

hence
( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds |.(n - k).| = 1 )

per cases
( ( |.(n - j1).| = 1 & i2 = j2 ) or ( |.(i2 - j2).| = 1 & n = j1 ) )
by A14, SEQM_3:42;

end;

suppose
( |.(n - j1).| = 1 & i2 = j2 )
; :: thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 )

|.(n - k).| = 1 )

hence
( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 ) by A8, A18, Th2; :: thesis: verum

end;|.(n - k).| = 1 ) by A8, A18, Th2; :: thesis: verum

suppose
( |.(i2 - j2).| = 1 & n = j1 )
; :: thesis: ( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 )

|.(n - k).| = 1 )

hence
( f /. (i + 1) in rng (Line (G,n)) or for k being Nat st f /. (i + 1) in rng (Line (G,k)) & k in dom G holds

|.(n - k).| = 1 ) by A17, A16, FUNCT_1:def 3; :: thesis: verum

end;|.(n - k).| = 1 ) by A17, A16, FUNCT_1:def 3; :: thesis: verum

|.(n - k).| = 1 ) ; :: thesis: verum