let k be Nat; for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & LSeg (f,k) is horizontal holds
ex j being Nat st
( 1 <= j & j <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 ) )
let G be Go-board; for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & LSeg (f,k) is horizontal holds
ex j being Nat st
( 1 <= j & j <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 ) )
let f be FinSequence of (TOP-REAL 2); ( f is_sequence_on G & LSeg (f,k) is horizontal implies ex j being Nat st
( 1 <= j & j <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 ) ) )
assume that
A1:
f is_sequence_on G
and
A2:
LSeg (f,k) is horizontal
; ex j being Nat st
( 1 <= j & j <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 ) )
per cases
( ( 1 <= k & k + 1 <= len f ) or not 1 <= k or not k + 1 <= len f )
;
suppose A3:
( 1
<= k &
k + 1
<= len f )
;
ex j being Nat st
( 1 <= j & j <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 ) )
k <= k + 1
by NAT_1:11;
then
k <= len f
by A3, XXREAL_0:2;
then consider i,
j being
Nat such that A4:
[i,j] in Indices G
and A5:
f /. k = G * (
i,
j)
by A1, A3, Lm2;
reconsider j =
j as
Nat ;
take
j
;
( 1 <= j & j <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 ) )thus A6:
( 1
<= j &
j <= width G )
by A4, MATRIX_0:32;
for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j)) `2 A7:
f /. k in LSeg (
f,
k)
by A3, TOPREAL1:21;
let p be
Point of
(TOP-REAL 2);
( p in LSeg (f,k) implies p `2 = (G * (1,j)) `2 )A8:
( 1
<= i &
i <= len G )
by A4, MATRIX_0:32;
assume
p in LSeg (
f,
k)
;
p `2 = (G * (1,j)) `2 hence p `2 =
(f /. k) `2
by A2, A7, SPPOL_1:def 2
.=
(G * (1,j)) `2
by A5, A6, A8, GOBOARD5:1
;
verum end;