let n, i be Nat; 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; 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); ( 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)) )
; ( 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;
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 )
; verum