let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. 1 in rng (Line (G,1)) & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G holds

( ( for i being Nat st 1 <= i & i <= len G holds

ex k being Nat st

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

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) )

let f be FinSequence of (TOP-REAL 2); :: thesis: ( 1 <= len f & f /. 1 in rng (Line (G,1)) & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G implies ( ( for i being Nat st 1 <= i & i <= len G holds

ex k being Nat st

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

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) ) )

assume that

A1: 1 <= len f and

A2: f /. 1 in rng (Line (G,1)) and

A3: f /. (len f) in rng (Line (G,(len G))) and

A4: f is_sequence_on G ; :: thesis: ( ( for i being Nat st 1 <= i & i <= len G holds

ex k being Nat st

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

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) )

A5: len f in dom f by A1, FINSEQ_3:25;

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len G implies ex k being Nat st

( k in dom f & f /. k in rng (Line (G,$1)) ) );

A6: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

thus A19: for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A18, A6); :: thesis: ( ( for i being Nat st 1 <= i & i <= len G & 2 <= len f holds

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) )

thus for i being Nat st 1 <= i & i <= len G & 2 <= len f holds

L~ f meets rng (Line (G,i)) :: thesis: for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j

n <= i ) & i < j & f /. j in rng (Line (G,k)) implies m < k )

assume that

A24: 1 <= m and

A25: m <= len G and

A26: ( 1 <= k & k <= len G ) and

A27: i in dom f and

A28: j in dom f and

A29: f /. i in rng (Line (G,m)) and

A30: for n being Nat st n in dom f & f /. n in rng (Line (G,m)) holds

n <= i and

A31: i < j and

A32: f /. j in rng (Line (G,k)) ; :: thesis: m < k

A33: ( i <= len f & j <= len f ) by A27, A28, FINSEQ_3:25;

( ( for i being Nat st 1 <= i & i <= len G holds

ex k being Nat st

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

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) )

let f be FinSequence of (TOP-REAL 2); :: thesis: ( 1 <= len f & f /. 1 in rng (Line (G,1)) & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G implies ( ( for i being Nat st 1 <= i & i <= len G holds

ex k being Nat st

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

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) ) )

assume that

A1: 1 <= len f and

A2: f /. 1 in rng (Line (G,1)) and

A3: f /. (len f) in rng (Line (G,(len G))) and

A4: f is_sequence_on G ; :: thesis: ( ( for i being Nat st 1 <= i & i <= len G holds

ex k being Nat st

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

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) )

A5: len f in dom f by A1, FINSEQ_3:25;

defpred S

( k in dom f & f /. k in rng (Line (G,$1)) ) );

A6: for k being Nat st S

S

proof

A18:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: ( 1 <= k & k <= len G implies ex i being Nat st

( i in dom f & f /. i in rng (Line (G,k)) ) ) ; :: thesis: S_{1}[k + 1]

assume that

A8: 1 <= k + 1 and

A9: k + 1 <= len G ; :: thesis: ex k being Nat st

( k in dom f & f /. k in rng (Line (G,(k + 1))) )

A10: k + 1 in dom G by A8, A9, FINSEQ_3:25;

end;assume A7: ( 1 <= k & k <= len G implies ex i being Nat st

( i in dom f & f /. i in rng (Line (G,k)) ) ) ; :: thesis: S

assume that

A8: 1 <= k + 1 and

A9: k + 1 <= len G ; :: thesis: ex k being Nat st

( k in dom f & f /. k in rng (Line (G,(k + 1))) )

A10: k + 1 in dom G by A8, A9, FINSEQ_3:25;

per cases
( k = 0 or k <> 0 )
;

end;

suppose A11:
k = 0
; :: thesis: ex k being Nat st

( k in dom f & f /. k in rng (Line (G,(k + 1))) )

( k in dom f & f /. k in rng (Line (G,(k + 1))) )

take
1
; :: thesis: ( 1 in dom f & f /. 1 in rng (Line (G,(k + 1))) )

thus ( 1 in dom f & f /. 1 in rng (Line (G,(k + 1))) ) by A1, A2, A11, FINSEQ_3:25; :: thesis: verum

end;thus ( 1 in dom f & f /. 1 in rng (Line (G,(k + 1))) ) by A1, A2, A11, FINSEQ_3:25; :: thesis: verum

suppose A12:
k <> 0
; :: thesis: ex k being Nat st

( k in dom f & f /. k in rng (Line (G,(k + 1))) )

( k in dom f & f /. k in rng (Line (G,(k + 1))) )

defpred S_{2}[ Nat] means ( $1 in dom f & f /. $1 in rng (Line (G,k)) );

A13: for i being Nat st S_{2}[i] holds

i <= len f by FINSEQ_3:25;

A14: 0 + 1 <= k by A12, NAT_1:13;

then A15: ex i being Nat st S_{2}[i]
by A7, A9, NAT_1:13;

consider m being Nat such that

A16: ( S_{2}[m] & ( for i being Nat st S_{2}[i] holds

i <= m ) ) from NAT_1:sch 6(A13, A15);

take m + 1 ; :: thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(k + 1))) )

k <= len G by A9, NAT_1:13;

then A17: k in dom G by A14, FINSEQ_3:25;

thus ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(k + 1))) ) by A1, A3, A4, A10, A17, A16, Th21; :: thesis: verum

end;A13: for i being Nat st S

i <= len f by FINSEQ_3:25;

A14: 0 + 1 <= k by A12, NAT_1:13;

then A15: ex i being Nat st S

consider m being Nat such that

A16: ( S

i <= m ) ) from NAT_1:sch 6(A13, A15);

take m + 1 ; :: thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(k + 1))) )

k <= len G by A9, NAT_1:13;

then A17: k in dom G by A14, FINSEQ_3:25;

thus ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(k + 1))) ) by A1, A3, A4, A10, A17, A16, Th21; :: thesis: verum

thus A19: for i being Nat holds S

L~ f meets rng (Line (G,i)) ) & ( for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j ) )

thus for i being Nat st 1 <= i & i <= len G & 2 <= len f holds

L~ f meets rng (Line (G,i)) :: thesis: for i, j, k, m being Nat st 1 <= i & i <= len G & 1 <= j & j <= len G & k in dom f & m in dom f & f /. k in rng (Line (G,i)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,i)) holds

n <= k ) & k < m & f /. m in rng (Line (G,j)) holds

i < j

proof

let m, k, i, j be Nat; :: thesis: ( 1 <= m & m <= len G & 1 <= k & k <= len G & i in dom f & j in dom f & f /. i in rng (Line (G,m)) & ( for n being Nat st n in dom f & f /. n in rng (Line (G,m)) holds
let i be Nat; :: thesis: ( 1 <= i & i <= len G & 2 <= len f implies L~ f meets rng (Line (G,i)) )

assume that

A20: ( 1 <= i & i <= len G ) and

A21: 2 <= len f ; :: thesis: L~ f meets rng (Line (G,i))

consider k being Nat such that

A22: k in dom f and

A23: f /. k in rng (Line (G,i)) by A19, A20;

f /. k in L~ f by A21, A22, Th1;

then (L~ f) /\ (rng (Line (G,i))) <> {} by A23, XBOOLE_0:def 4;

hence L~ f meets rng (Line (G,i)) ; :: thesis: verum

end;assume that

A20: ( 1 <= i & i <= len G ) and

A21: 2 <= len f ; :: thesis: L~ f meets rng (Line (G,i))

consider k being Nat such that

A22: k in dom f and

A23: f /. k in rng (Line (G,i)) by A19, A20;

f /. k in L~ f by A21, A22, Th1;

then (L~ f) /\ (rng (Line (G,i))) <> {} by A23, XBOOLE_0:def 4;

hence L~ f meets rng (Line (G,i)) ; :: thesis: verum

n <= i ) & i < j & f /. j in rng (Line (G,k)) implies m < k )

assume that

A24: 1 <= m and

A25: m <= len G and

A26: ( 1 <= k & k <= len G ) and

A27: i in dom f and

A28: j in dom f and

A29: f /. i in rng (Line (G,m)) and

A30: for n being Nat st n in dom f & f /. n in rng (Line (G,m)) holds

n <= i and

A31: i < j and

A32: f /. j in rng (Line (G,k)) ; :: thesis: m < k

A33: ( i <= len f & j <= len f ) by A27, A28, FINSEQ_3:25;

per cases
( m = len G or m <> len G )
;

end;

suppose
m <> len G
; :: thesis: m < k

then
m < len G
by A25, XXREAL_0:1;

then ( 1 <= m + 1 & m + 1 <= len G ) by NAT_1:11, NAT_1:13;

then A34: m + 1 in dom G by FINSEQ_3:25;

reconsider l = j - i as Element of NAT by A31, INT_1:5;

defpred S_{2}[ set ] means for n, l being Nat st n = $1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Line (G,l)) & l in dom G holds

m < l;

A35: k in dom G by A26, FINSEQ_3:25;

m in dom G by A24, A25, FINSEQ_3:25;

then A36: f /. (i + 1) in rng (Line (G,(m + 1))) by A1, A3, A4, A27, A29, A30, A34, Th21;

A37: for o being Nat st S_{2}[o] holds

S_{2}[o + 1]
_{2}[ 0 ]
;

A52: for o being Nat holds S_{2}[o]
from NAT_1:sch 2(A51, A37);

( 0 < j - i & i + l = j ) by A31, XREAL_1:50;

hence m < k by A28, A32, A52, A35; :: thesis: verum

end;then ( 1 <= m + 1 & m + 1 <= len G ) by NAT_1:11, NAT_1:13;

then A34: m + 1 in dom G by FINSEQ_3:25;

reconsider l = j - i as Element of NAT by A31, INT_1:5;

defpred S

m < l;

A35: k in dom G by A26, FINSEQ_3:25;

m in dom G by A24, A25, FINSEQ_3:25;

then A36: f /. (i + 1) in rng (Line (G,(m + 1))) by A1, A3, A4, A27, A29, A30, A34, Th21;

A37: for o being Nat st S

S

proof

A51:
S
let o be Nat; :: thesis: ( S_{2}[o] implies S_{2}[o + 1] )

assume A38: S_{2}[o]
; :: thesis: S_{2}[o + 1]

let n, l be Nat; :: thesis: ( n = o + 1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Line (G,l)) & l in dom G implies m < l )

assume that

A39: n = o + 1 and

A40: n > 0 and

A41: i + n in dom f and

A42: f /. (i + n) in rng (Line (G,l)) and

A43: l in dom G ; :: thesis: m < l

end;assume A38: S

let n, l be Nat; :: thesis: ( n = o + 1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Line (G,l)) & l in dom G implies m < l )

assume that

A39: n = o + 1 and

A40: n > 0 and

A41: i + n in dom f and

A42: f /. (i + n) in rng (Line (G,l)) and

A43: l in dom G ; :: thesis: m < l

per cases
( o = 0 or o <> 0 )
;

end;

suppose A44:
o <> 0
; :: thesis: m < l

1 <= i
by A27, FINSEQ_3:25;

then A45: 1 <= i + o by NAT_1:12;

( i + n <= len f & i + o <= (i + o) + 1 ) by A41, FINSEQ_3:25, NAT_1:12;

then i + o <= len f by A39, XXREAL_0:2;

then A46: i + o in dom f by A45, FINSEQ_3:25;

then consider l1 being Nat such that

A47: l1 in dom G and

A48: f /. (i + o) in rng (Line (G,l1)) by A4, Th19;

A49: m < l1 by A38, A44, A46, A47, A48;

A50: i + n = (i + o) + 1 by A39;

end;then A45: 1 <= i + o by NAT_1:12;

( i + n <= len f & i + o <= (i + o) + 1 ) by A41, FINSEQ_3:25, NAT_1:12;

then i + o <= len f by A39, XXREAL_0:2;

then A46: i + o in dom f by A45, FINSEQ_3:25;

then consider l1 being Nat such that

A47: l1 in dom G and

A48: f /. (i + o) in rng (Line (G,l1)) by A4, Th19;

A49: m < l1 by A38, A44, A46, A47, A48;

A50: i + n = (i + o) + 1 by A39;

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

|.(l1 - k).| = 1 ) by A4, A41, A50, A46, A47, A48, Th20;

end;

|.(l1 - k).| = 1 ) by A4, A41, A50, A46, A47, A48, Th20;

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

|.(l1 - k).| = 1 ; :: thesis: m < l

|.(l1 - k).| = 1 ; :: thesis: m < l

then
|.(l1 - l).| = 1
by A42, A43;

end;A52: for o being Nat holds S

( 0 < j - i & i + l = j ) by A31, XREAL_1:50;

hence m < k by A28, A32, A52, A35; :: thesis: verum