let k be Nat; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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); :: thesis: ( 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) ; :: thesis: 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 ;
:: thesis: verum

end;

suppose A9: ( not 1 <= k or not k + 1 <= len f ) ; :: thesis: 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 ) )

take 1 ; :: thesis: ( 1 <= 1 & 1 <= width G & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,1)) `2 ) )
width G <> 0 by MATRIX_0:def 10;
hence ( 1 <= 1 & 1 <= width G ) by NAT_1:14; :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,1)) `2
thus for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,1)) `2 by A9, TOPREAL1:def 3; :: thesis: verum

end;

end;