let n, k be Nat; :: thesis: for G being Go-board
for f being FinSequence of () st k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) holds
( ( for i being Nat st k <= i & i <= len G holds
ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Nat st k < i & i <= len G holds
ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )

let G be Go-board; :: thesis: for f being FinSequence of () st k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) holds
( ( for i being Nat st k <= i & i <= len G holds
ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Nat st k < i & i <= len G holds
ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )

let f be FinSequence of (); :: thesis: ( k in dom G & f is_sequence_on G & f /. (len f) in rng (Line (G,(len G))) & n in dom f & f /. n in rng (Line (G,k)) implies ( ( for i being Nat st k <= i & i <= len G holds
ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Nat st k < i & i <= len G holds
ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) ) )

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: ( ( for i being Nat st k <= i & i <= len G holds
ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,i)) ) ) & ( for i being Nat st k < i & i <= len G holds
ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) ) )

defpred S1[ 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 ;
A6: ( 1 <= n & n <= len f ) by ;
A7: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A8: S1[i] ; :: thesis: S1[i + 1]
assume that
A9: k <= i + 1 and
A10: i + 1 <= len G ; :: thesis: ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )

per cases ( k = i + 1 or k < i + 1 ) by ;
suppose A11: k = i + 1 ; :: thesis: ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )

take j = n; :: thesis: ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )
thus ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) ) by A3, A4, A11; :: thesis: verum
end;
suppose A12: k < i + 1 ; :: thesis: ex j being Nat st
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )

then k <= i by NAT_1:13;
then A13: 1 <= i by ;
i <= len G by ;
then A14: i in dom G by ;
1 <= i + 1 by ;
then A15: i + 1 in dom G by ;
defpred S2[ Nat] means ( \$1 in dom f & n <= \$1 & f /. \$1 in rng (Line (G,i)) );
A16: for j being Nat st S2[j] holds
j <= len f by FINSEQ_3:25;
A17: ex j being Nat st S2[j] by ;
consider ma being Nat such that
A18: ( S2[ma] & ( for j being Nat st S2[j] holds
j <= ma ) ) from
A19: now :: thesis: for j being Nat st j in dom f & f /. j in rng (Line (G,i)) holds
j <= ma
let j be Nat; :: thesis: ( j in dom f & f /. j in rng (Line (G,i)) implies j <= ma )
assume A20: ( j in dom f & f /. j in rng (Line (G,i)) ) ; :: thesis: j <= ma
now :: thesis: j <= ma
per cases ( j < n or n <= j ) ;
suppose j < n ; :: thesis: j <= ma
hence j <= ma by ; :: thesis: verum
end;
suppose n <= j ; :: thesis: j <= ma
hence j <= ma by ; :: thesis: verum
end;
end;
end;
hence j <= ma ; :: thesis: verum
end;
take j = ma + 1; :: thesis: ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )
A21: 1 <= len f by ;
hence j in dom f by A2, A14, A15, A18, A19, Th21; :: thesis: ( n <= j & f /. j in rng (Line (G,(i + 1))) )
ma <= ma + 1 by NAT_1:11;
hence ( n <= j & f /. j in rng (Line (G,(i + 1))) ) by ; :: thesis: verum
end;
end;
end;
A22: S1[ 0 ] by ;
thus A23: for i being Nat holds S1[i] from NAT_1:sch 2(A22, A7); :: thesis: for i being Nat st k < i & i <= len G holds
ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) )

let i be Nat; :: thesis: ( k < i & i <= len G implies ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) ) )

assume that
A24: k < i and
A25: i <= len G ; :: thesis: ex j being Nat st
( j in dom f & n < j & f /. j in rng (Line (G,i)) )

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 ;
take j ; :: thesis: ( j in dom f & n < j & f /. j in rng (Line (G,i)) )
thus j in dom f by A26; :: thesis: ( n < j & f /. j in rng (Line (G,i)) )
1 <= i by ;
then i in dom G by ;
then n <> j by A1, A4, A24, A28, Th2;
hence ( n < j & f /. j in rng (Line (G,i)) ) by ; :: thesis: verum