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

proof

let k be Element of NAT ; :: thesis:
assume A7: ( 1 <= k & k <= width G implies ex i being Element of NAT st
( i in dom f & f /. i in rng (Col G,k) ) ) ; :: thesis:
assume A8: ( 1 <= k + 1 & k + 1 <= width G ) ; :: thesis:
then A9: k + 1 in Seg (width G) by FINSEQ_1:3;

per cases ;

suppose A10: k = 0 ; :: thesis:

take i = 1; :: thesis:
thus ( i in dom f & f /. i in rng (Col G,(k + 1)) ) by A1, A10, FINSEQ_3:27; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then ( 0 < k & k <= k + 1 ) by NAT_1:11;
then A11: ( 0 + 1 <= k & k <= width G ) by A8, NAT_1:13;
defpred S₂[ Nat] means ( $1 in dom f & f /. $1 in rng (Col G,k) );
A12: ex i being Nat st S₂[i] by A7, A11;
A13: for i being Nat st S₂[i] holds
i <= len f by FINSEQ_3:27;
A14: k in Seg (width G) by A11, FINSEQ_1:3;
consider m being Nat such that
A15: ( S₂[m] & ( for i being Nat st S₂[i] holds
i <= m ) ) from NAT_1:sch 6(A13, A12);
take n = m + 1; :: thesis:
for i being Element of NAT st S₂[i] holds
i <= m by A15;
hence ( n in dom f & f /. n in rng (Col G,(k + 1)) ) by A1, A2, A3, A9, A14, A15, Th48; :: thesis:

end;

thus A16: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A5, A6); :: thesis:
thus for i being Element of NAT st 1 <= i & i <= width G & 2 <= len f holds
L~ f meets rng (Col G,i) :: thesis:

proof

let i be Element of NAT ; :: thesis:
assume A17: ( 1 <= i & i <= width G & 2 <= len f ) ; :: thesis:
then consider k being Element of NAT such that
A18: ( k in dom f & f /. k in rng (Col G,i) ) by A16;
f /. k in L~ f by A17, A18, Th16;
then (L~ f) /\ (rng (Col G,i)) <> {} by A18, XBOOLE_0:def 4;
hence L~ f meets rng (Col G,i) by XBOOLE_0:def 7; :: thesis:

end;

let m, k, i, j be Element of NAT ; :: thesis:
assume A19: ( 1 <= m & m <= width G & 1 <= k & k <= width G & i in dom f & j in dom f & f /. i in rng (Col G,m) & ( for n being Element of NAT st n in dom f & f /. n in rng (Col G,m) holds
n <= i ) & i < j & f /. j in rng (Col G,k) ) ; :: thesis:
then A20: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) by FINSEQ_3:27;

now

per cases ;

case m = width G ; :: thesis:

then len f <= i by A2, A4, A19;
hence contradiction by A19, A20, XXREAL_0:1; :: thesis:

end;

case m <> width G ; :: thesis:

then m < width G by A19, XXREAL_0:1;
then ( 1 <= m + 1 & m + 1 <= width G ) by NAT_1:11, NAT_1:13;
then ( m + 1 in Seg (width G) & m in Seg (width G) ) by A19, FINSEQ_1:3;
then A21: ( i + 1 in dom f & f /. (i + 1) in rng (Col G,(m + 1)) & m + 1 in Seg (width G) ) by A1, A2, A3, A19, Th48;
defpred S₂[ set ] means for n, l being Element of 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;
A22: S₂[ 0 ] ;
A23: for o being Element of NAT st S₂[o] holds
S₂[o + 1]

proof

let o be Element of NAT ; :: thesis:
assume A24: S₂[o] ; :: thesis:
let n, l be Element of NAT ; :: thesis:
assume A25: ( n = o + 1 & n > 0 & i + n in dom f & f /. (i + n) in rng (Col G,l) & l in Seg (width G) ) ; :: thesis:

now

per cases ;

suppose o = 0 ; :: thesis:

then ( l = m + 1 & m < m + 1 ) by A21, A25, Th20, NAT_1:13;
hence m < l ; :: thesis:

end;

suppose o <> 0 ; :: thesis:

then A26: 0 < o ;
A27: ( 1 <= i & i + n <= len f & i + n = (i + o) + 1 & i + o <= (i + o) + 1 & i <= i + o ) by A19, A25, FINSEQ_3:27, NAT_1:12;
then ( 1 <= i + o & i + o <= len f ) by XXREAL_0:2;
then A28: i + o in dom f by FINSEQ_3:27;
then consider l1 being Element of NAT such that
A29: ( l1 in Seg (width G) & f /. (i + o) in rng (Col G,l1) ) by A3, Th46;
A30: m < l1 by A24, A26, A28, A29;

now

per cases by A3, A25, A27, A28, A29, Th47;

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

hence m < l by A25, A29, A30, Th20; :: thesis:

end;

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

then A31: abs (l1 - l) = 1 by A25;

now

per cases by A31, Th1;

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

then A32: m <= l by A30, NAT_1:13;

now

per cases by A32, XXREAL_0:1;

case m = l ; :: thesis:

then i + n <= i by A19, A25;
then n <= i - i by XREAL_1:21;
hence contradiction by A25; :: thesis:

end;

case m < l ; :: thesis:

hence m < l ; :: thesis:

end;

hence m < l ; :: thesis:

end;

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

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

end;

hence m < l ; :: thesis:

end;

hence m < l ; :: thesis:

end;

hence m < l ; :: thesis:

end;

A33: for o being Element of NAT holds S₂[o] from NAT_1:sch 1(A22, A23);
A34: ( 0 < j - i & i <= j ) by A19, XREAL_1:52;
reconsider l = j - i as Element of NAT by A19, INT_1:18;
( i + l = j & k in Seg (width G) ) by A19, FINSEQ_1:3;
hence m < k by A19, A33, A34; :: thesis:

end;

hence m < k ; :: thesis: