let n, k be Nat; :: thesis: for G being Go-board

for f being FinSequence of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 S_{1}[ 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_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
by A1, FINSEQ_3:25;

thus A23: for i being Nat holds S_{1}[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 A23, A24, A25;

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 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: verum

for f being FinSequence of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 S

( 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

S

proof

A22:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A8: S_{1}[i]
; :: thesis: S_{1}[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))) )

end;assume A8: S

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 A9, XXREAL_0:1;

end;

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))) )

( 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;thus ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) ) by A3, A4, A11; :: thesis: verum

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))) )

( 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 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_{2}[ Nat] means ( $1 in dom f & n <= $1 & f /. $1 in rng (Line (G,i)) );

A16: for j being Nat st S_{2}[j] holds

j <= len f by FINSEQ_3:25;

A17: ex j being Nat st S_{2}[j]
by A8, A10, A12, NAT_1:13;

consider ma being Nat such that

A18: ( S_{2}[ma] & ( for j being Nat st S_{2}[j] holds

j <= ma ) ) from NAT_1:sch 6(A16, A17);

A21: 1 <= len f by A6, XXREAL_0:2;

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 A2, A14, A15, A18, A21, A19, Th21, XXREAL_0:2; :: thesis: verum

end;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

A16: for j being Nat st S

j <= len f by FINSEQ_3:25;

A17: ex j being Nat st S

consider ma being Nat such that

A18: ( S

j <= ma ) ) from NAT_1:sch 6(A16, A17);

A19: now :: thesis: for j being Nat st j in dom f & f /. j in rng (Line (G,i)) holds

j <= ma

take j = ma + 1; :: thesis: ( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )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

hence j <= ma ; :: thesis: verum

end;assume A20: ( j in dom f & f /. j in rng (Line (G,i)) ) ; :: thesis: j <= ma

hence j <= ma ; :: thesis: verum

A21: 1 <= len f by A6, XXREAL_0:2;

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 A2, A14, A15, A18, A21, A19, Th21, XXREAL_0:2; :: thesis: verum

thus A23: for i being Nat holds S

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 A23, A24, A25;

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 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: verum