let n, k be 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 & f /. (len f) in rng (Line (G,(len G))) ) and
A3: n in dom f and
A4: f /. n in rng (Line (G,k)) ; :: thesis:
defpred S₁[ Nat] means ( k <= $1 & $1 <= len G implies ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,$1)) ) );
A5: 1 <= k by A1, FINSEQ_3:25;
A6: ( 1 <= n & n <= len f ) by A3, FINSEQ_3:25;
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A8: S₁[i] ; :: thesis:
assume that
A9: k <= i + 1 and
A10: i + 1 <= len G ; :: thesis:

per cases by A9, XXREAL_0:1;

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

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

end;

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

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

A19: now :: thesis:

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

now :: thesis:

per cases ;

suppose j < n ; :: thesis:

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

end;

suppose n <= j ; :: thesis:

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

end;

end;

end;

hence j <= ma ; :: thesis:

end;

take j = ma + 1; :: thesis:
A21: 1 <= len f by A6, XXREAL_0:2;
hence j in dom f by A2, A14, A15, A18, A19, Th21; :: thesis:
ma <= ma + 1 by NAT_1:11;
hence ( n <= j & f /. j in rng (Line (G,(i + 1))) ) by A2, A14, A15, A18, A21, A19, Th21, XXREAL_0:2; :: thesis:

end;

end;

end;

A22: S₁[ 0 ] by A1, FINSEQ_3:25;
thus A23: for i being Nat holds S₁[i] from NAT_1:sch 2(A22, A7); :: thesis:
let i be Nat; :: thesis:
assume that
A24: k < i and
A25: i <= len G ; :: thesis:
consider j being Nat such that
A26: j in dom f and
A27: n <= j and
A28: f /. j in rng (Line (G,i)) by A23, A24, A25;
take j ; :: thesis:
thus j in dom f by A26; :: thesis:
1 <= i by A5, A24, XXREAL_0:2;
then i in dom G by A25, FINSEQ_3:25;
then n <> j by A1, A4, A24, A28, Th2;
hence ( n < j & f /. j in rng (Line (G,i)) ) by A27, A28, XXREAL_0:1; :: thesis: