let f be non empty FinSequence of (TOP-REAL 2); :: thesis:
let k be Nat; :: thesis:
assume A1: LSeg (f,k) is horizontal ; :: thesis:

suppose A2: ( 1 <= k & k + 1 <= len f ) ; :: thesis:

k <= k + 1 by NAT_1:11;
then k <= len f by A2, XXREAL_0:2;
then k in dom f by A2, FINSEQ_3:25;
then consider i, j being Nat such that
A3: [i,j] in Indices (GoB f) and
A4: f /. k = (GoB f) * (i,j) by GOBOARD2:14;
take j ; :: thesis:
thus A5: ( 1 <= j & j <= width (GoB f) ) by A3, MATRIX_0:32; :: thesis:
A6: f /. k in LSeg (f,k) by A2, TOPREAL1:21;
let p be Point of (TOP-REAL 2); :: thesis:
A7: ( 1 <= i & i <= len (GoB f) ) by A3, MATRIX_0:32;
assume p in LSeg (f,k) ; :: thesis:
hence p `2 = (f /. k) `2 by A1, A6, SPPOL_1:def 2
.= ((GoB f) * (1,j)) `2 by A4, A5, A7, GOBOARD5:1 ;
:: thesis:

end;

suppose A8: ( not 1 <= k or not k + 1 <= len f ) ; :: thesis:

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

end;

end;