let n, k be Nat; 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; 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); ( 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))
; ( ( 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 A1, FINSEQ_3:25;
A6:
( 1 <= n & n <= len f )
by A3, FINSEQ_3:25;
A7:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A8:
S1[
i]
;
S1[i + 1]
assume that A9:
k <= i + 1
and A10:
i + 1
<= len G
;
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;
suppose A12:
k < i + 1
;
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 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 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 A8, A10, A12, NAT_1:13;
consider ma being
Nat such that A18:
(
S2[
ma] & ( for
j being
Nat st
S2[
j] holds
j <= ma ) )
from NAT_1:sch 6(A16, A17);
take j =
ma + 1;
( j in dom f & n <= j & f /. j in rng (Line (G,(i + 1))) )A21:
1
<= len f
by A6, XXREAL_0:2;
hence
j in dom f
by A2, A14, A15, A18, A19, Th21;
( 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;
verum end; end;
end;
A22:
S1[ 0 ]
by A1, FINSEQ_3:25;
thus A23:
for i being Nat holds S1[i]
from NAT_1:sch 2(A22, A7); 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; ( 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
; 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
; ( j in dom f & n < j & f /. j in rng (Line (G,i)) )
thus
j in dom f
by A26; ( 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; verum