let G be Go-board; :: thesis: for f being FinSequence of () 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 (); :: 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 ;
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[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: S1[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 ;
per cases ( k = 0 or k <> 0 ) ;
suppose A11: k = 0 ; :: thesis: ex k being Nat st
( 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 ; :: thesis: verum
end;
suppose A12: k <> 0 ; :: thesis: ex k being Nat st
( k in dom f & f /. k in rng (Line (G,(k + 1))) )

defpred S2[ Nat] means ( \$1 in dom f & f /. \$1 in rng (Line (G,k)) );
A13: for i being Nat st S2[i] holds
i <= len f by FINSEQ_3:25;
A14: 0 + 1 <= k by ;
then A15: ex i being Nat st S2[i] by ;
consider m being Nat such that
A16: ( S2[m] & ( for i being Nat st S2[i] holds
i <= m ) ) from take m + 1 ; :: thesis: ( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(k + 1))) )
k <= len G by ;
then A17: k in dom G by ;
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;
end;
end;
A18: S1[ 0 ] ;
thus A19: for i being Nat holds S1[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
proof
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 ;
f /. k in L~ f by ;
then (L~ f) /\ (rng (Line (G,i))) <> {} by ;
hence L~ f meets rng (Line (G,i)) ; :: thesis: verum
end;
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
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 ;
per cases ( m = len G or m <> len G ) ;
suppose m = len G ; :: thesis: m < k
then len f <= i by A3, A5, A30;
hence m < k by ; :: thesis: verum
end;
suppose m <> len G ; :: thesis: m < k
then m < len G by ;
then ( 1 <= m + 1 & m + 1 <= len G ) by ;
then A34: m + 1 in dom G by FINSEQ_3:25;
reconsider l = j - i as Element of NAT by ;
defpred S2[ 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 ;
m in dom G by ;
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 S2[o] holds
S2[o + 1]
proof
let o be Nat; :: thesis: ( S2[o] implies S2[o + 1] )
assume A38: S2[o] ; :: thesis: S2[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
per cases ( o = 0 or o <> 0 ) ;
suppose A44: o <> 0 ; :: thesis: m < l
1 <= i by ;
then A45: 1 <= i + o by NAT_1:12;
( i + n <= len f & i + o <= (i + o) + 1 ) by ;
then i + o <= len f by ;
then A46: i + o in dom f by ;
then consider l1 being Nat such that
A47: l1 in dom G and
A48: f /. (i + o) in rng (Line (G,l1)) by ;
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;
suppose f /. (i + n) in rng (Line (G,l1)) ; :: thesis: m < l
hence m < l by A42, A43, A47, A49, Th2; :: thesis: verum
end;
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
then |.(l1 - l).| = 1 by ;
per cases then ( ( l1 > l & l1 = l + 1 ) or ( l1 < l & l = l1 + 1 ) ) by SEQM_3:41;
suppose ( l1 > l & l1 = l + 1 ) ; :: thesis: m < l
then m <= l by ;
per cases then ( m = l or m < l ) by XXREAL_0:1;
suppose m = l ; :: thesis: m < l
then i + n <= i by ;
then n <= i - i by XREAL_1:19;
hence m < l by A40; :: thesis: verum
end;
suppose m < l ; :: thesis: m < l
hence m < l ; :: thesis: verum
end;
end;
end;
suppose ( l1 < l & l = l1 + 1 ) ; :: thesis: m < l
hence m < l by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A51: S2[ 0 ] ;
A52: for o being Nat holds S2[o] from ( 0 < j - i & i + l = j ) by ;
hence m < k by A28, A32, A52, A35; :: thesis: verum
end;
end;