let G be Go-board; :: thesis:
let f be FinSequence of (TOP-REAL 2); :: thesis:
assume that
A1: 1 <= len f and
A2: f /. 1 in rng (Col (G,1)) and
A3: f /. (len f) in rng (Col (G,(width G))) and
A4: f is_sequence_on G ; :: thesis:
A5: len f in dom f by A1, FINSEQ_3:25;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= width G implies ex k being Nat st
( k in dom f & f /. k in rng (Col (G,$1)) ) );
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A7: ( 1 <= k & k <= width G implies ex i being Nat st
( i in dom f & f /. i in rng (Col (G,k)) ) ) ; :: thesis:
assume that
A8: 1 <= k + 1 and
A9: k + 1 <= width G ; :: thesis:
A10: k + 1 in Seg (width G) by A8, A9, FINSEQ_1:1;

per cases ;

suppose A11: k = 0 ; :: thesis:

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

end;

suppose A12: k <> 0 ; :: thesis:

defpred S₂[ Nat] means ( $1 in dom f & f /. $1 in rng (Col (G,k)) );
A13: for i being Nat st S₂[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₂[i] by A7, A9, NAT_1:13;
consider m being Nat such that
A16: ( S₂[m] & ( for i being Nat st S₂[i] holds
i <= m ) ) from NAT_1:sch 6(A13, A15);
take m + 1 ; :: thesis:
k <= width G by A9, NAT_1:13;
then A17: k in Seg (width G) by A14, FINSEQ_1:1;
thus ( m + 1 in dom f & f /. (m + 1) in rng (Col (G,(k + 1))) ) by A1, A3, A4, A10, A17, A16, Th25; :: thesis:

end;

end;

end;

A18: S₁[ 0 ] ;
thus A19: for i being Nat holds S₁[i] from NAT_1:sch 2(A18, A6); :: thesis:
thus for i being Nat st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col (G,i)) :: thesis:

proof

let i be Nat; :: thesis:
assume that
A20: ( 1 <= i & i <= width G ) and
A21: 2 <= len f ; :: thesis:
consider k being Nat such that
A22: k in dom f and
A23: f /. k in rng (Col (G,i)) by A19, A20;
f /. k in L~ f by A21, A22, Th1;
then (L~ f) /\ (rng (Col (G,i))) <> {} by A23, XBOOLE_0:def 4;
hence L~ f meets rng (Col (G,i)) ; :: thesis:

end;

let m, k, i, j be Nat; :: thesis:
assume that
A24: 1 <= m and
A25: m <= width G and
A26: ( 1 <= k & k <= width G ) and
A27: i in dom f and
A28: j in dom f and
A29: f /. i in rng (Col (G,m)) and
A30: for n being Nat st n in dom f & f /. n in rng (Col (G,m)) holds
n <= i and
A31: i < j and
A32: f /. j in rng (Col (G,k)) ; :: thesis:
A33: ( i <= len f & j <= len f ) by A27, A28, FINSEQ_3:25;

now :: thesis:

per cases ;

case m = width G ; :: thesis:

then len f <= i by A3, A5, A30;
hence contradiction by A31, A33, XXREAL_0:1; :: thesis:

end;

case m <> width G ; :: thesis:

then m < width G by A25, XXREAL_0:1;
then ( 1 <= m + 1 & m + 1 <= width G ) by NAT_1:11, NAT_1:13;
then A34: m + 1 in Seg (width G) by FINSEQ_1:1;
reconsider l = j - i as Element of NAT by A31, INT_1:5;
defpred S₂[ set ] means for n, l being Nat st n = $1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Col (G,l)) & l in Seg (width G) holds
m < l;
A35: k in Seg (width G) by A26, FINSEQ_1:1;
m in Seg (width G) by A24, A25, FINSEQ_1:1;
then A36: f /. (i + 1) in rng (Col (G,(m + 1))) by A1, A3, A4, A27, A29, A30, A34, Th25;
A37: for o being Nat st S₂[o] holds
S₂[o + 1]

proof

let o be Nat; :: thesis:
assume A38: S₂[o] ; :: thesis:
let n, l be Nat; :: thesis:
assume that
A39: n = o + 1 and
A40: n > 0 and
A41: i + n in dom f and
A42: f /. (i + n) in rng (Col (G,l)) and
A43: l in Seg (width G) ; :: thesis:

now :: thesis:

per cases ;

suppose o = 0 ; :: thesis:

then l = m + 1 by A34, A36, A39, A42, A43, Th3;
hence m < l by NAT_1:13; :: thesis:

end;

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

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 Seg (width G) and
A48: f /. (i + o) in rng (Col (G,l1)) by A4, Th23;
A49: m < l1 by A38, A44, A46, A47, A48;
A50: i + n = (i + o) + 1 by A39;

now :: thesis:

per cases by A4, A41, A50, A46, A47, A48, Th24;

suppose f /. (i + n) in rng (Col (G,l1)) ; :: thesis:

hence m < l by A42, A43, A47, A49, Th3; :: thesis:

end;

suppose for k being Nat st f /. (i + n) in rng (Col (G,k)) & k in Seg (width G) holds
|.(l1 - k).| = 1 ; :: thesis:

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

now :: thesis:

per cases by A51, SEQM_3:41;

suppose ( l1 > l & l1 = l + 1 ) ; :: thesis:

then A52: m <= l by A49, NAT_1:13;

now :: thesis:

per cases by A52, XXREAL_0:1;

case m = l ; :: thesis:

then i + n <= i by A30, A41, A42;
then n <= i - i by XREAL_1:19;
hence contradiction by A40; :: thesis:

end;

case m < l ; :: thesis:

hence m < l ; :: thesis:

end;

end;

end;

hence m < l ; :: thesis:

end;

suppose ( l1 < l & l = l1 + 1 ) ; :: thesis:

hence m < l by A49, XXREAL_0:2; :: thesis:

end;

end;

end;

hence m < l ; :: thesis:

end;

end;

end;

hence m < l ; :: thesis:

end;

end;

end;

hence m < l ; :: thesis:

end;

A53: S₂[ 0 ] ;
A54: for o being Nat holds S₂[o] from NAT_1:sch 2(A53, A37);
( 0 < j - i & i + l = j ) by A31, XREAL_1:50;
hence m < k by A28, A32, A54, A35; :: thesis:

end;

end;

end;

hence m < k ; :: thesis: