let f be non empty FinSequence of (); :: thesis: for k being Nat st LSeg (f,k) is horizontal holds
ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) )

let k be Nat; :: thesis: ( LSeg (f,k) is horizontal implies ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) ) )

assume A1: LSeg (f,k) is horizontal ; :: thesis: ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) )

per cases ( ( 1 <= k & k + 1 <= len f ) or not 1 <= k or not k + 1 <= len f ) ;
suppose A2: ( 1 <= k & k + 1 <= len f ) ; :: thesis: ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) )

k <= k + 1 by NAT_1:11;
then k <= len f by ;
then k in dom f by ;
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: ( 1 <= j & j <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) )

thus A5: ( 1 <= j & j <= width (GoB f) ) by ; :: thesis: for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2

A6: f /. k in LSeg (f,k) by ;
let p be Point of (); :: thesis: ( p in LSeg (f,k) implies p `2 = ((GoB f) * (1,j)) `2 )
A7: ( 1 <= i & i <= len (GoB f) ) by ;
assume p in LSeg (f,k) ; :: thesis: p `2 = ((GoB f) * (1,j)) `2
hence p `2 = (f /. k) `2 by
.= ((GoB f) * (1,j)) `2 by ;
:: thesis: verum
end;
suppose A8: ( not 1 <= k or not k + 1 <= len f ) ; :: thesis: ex j being Nat st
( 1 <= j & j <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,j)) `2 ) )

take 1 ; :: thesis: ( 1 <= 1 & 1 <= width (GoB f) & ( for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,1)) `2 ) )

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

thus for p being Point of () st p in LSeg (f,k) holds
p `2 = ((GoB f) * (1,1)) `2 by ; :: thesis: verum
end;
end;