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

let i be Element of NAT ; :: thesis:
assume A10: S₁[i] ; :: thesis:
assume A11: ( k <= i + 1 & i + 1 <= len G ) ; :: thesis:

per cases by A11, XXREAL_0:1;

suppose A12: k = i + 1 ; :: thesis:

take j = n; :: thesis:
thus ( j in dom f & n <= j & f /. j in rng (Line G,(i + 1)) ) by A4, A5, A12; :: thesis:

end;

suppose A13: k < i + 1 ; :: thesis:

then ( k <= i & i <= i + 1 & k <= i + 1 ) by NAT_1:13;
then ( 1 <= i & i <= len G & 1 <= i + 1 & k <= i ) by A6, A11, XXREAL_0:2;
then A14: ( i in dom G & i + 1 in dom G ) by A11, FINSEQ_3:27;
defpred S₂[ Nat] means ( $1 in dom f & n <= $1 & f /. $1 in rng (Line G,i) );
A15: ex j being Nat st S₂[j] by A10, A11, A13, NAT_1:13;
A16: for j being Nat st S₂[j] holds
j <= len f by FINSEQ_3:27;
consider ma being Nat such that
A17: ( S₂[ma] & ( for j being Nat st S₂[j] holds
j <= ma ) ) from NAT_1:sch 6(A16, A15);
A18: 1 <= len f by A7, XXREAL_0:2;

A19: now

let j be Element of NAT ; :: thesis:
assume A20: ( j in dom f & f /. j in rng (Line G,i) ) ; :: thesis:

per cases ;

suppose j < n ; :: thesis:

hence j <= ma by A17, XXREAL_0:2; :: thesis:

end;

suppose n <= j ; :: thesis:

hence j <= ma by A17, A20; :: thesis:

end;

hence j <= ma ; :: thesis:

end;

take j = ma + 1; :: thesis:
thus j in dom f by A2, A3, A14, A17, A18, A19, Th44; :: thesis:
ma <= ma + 1 by NAT_1:11;
hence ( n <= j & f /. j in rng (Line G,(i + 1)) ) by A2, A3, A14, A17, A18, A19, Th44, XXREAL_0:2; :: thesis:

end;

hence ex j being Element of NAT st
( j in dom f & n <= j & f /. j in rng (Line G,(i + 1)) ) ; :: thesis:

end;

thus A21: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A8, A9); :: thesis:
let i be Element of NAT ; :: thesis:
assume A22: ( k < i & i <= len G ) ; :: thesis:
then consider j being Element of NAT such that
A23: ( j in dom f & n <= j & f /. j in rng (Line G,i) ) by A21;
1 <= i by A6, A22, XXREAL_0:2;
then A24: i in dom G by A22, FINSEQ_3:27;
take j ; :: thesis:
thus j in dom f by A23; :: thesis:
n <> j by A1, A5, A22, A23, A24, Th19;
hence ( n < j & f /. j in rng (Line G,i) ) by A23, XXREAL_0:1; :: thesis: