let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for k being Element of NAT st LSeg f,k is horizontal holds
ex j being Element of NAT st
( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `2 = ((GoB f) * 1,j) `2 ) )
let k be Element of NAT ; :: thesis: ( LSeg f,k is horizontal implies ex j being Element of NAT st
( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) 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 Element of NAT st
( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) 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 Element of NAT st
( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) 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 A2, XXREAL_0:2;
then k in dom f by A2, FINSEQ_3:27;
then consider i, j being Element of NAT such that
A3: [i,j] in Indices (GoB f) and
A4: f /. k = (GoB f) * i,j by GOBOARD2:25;
take j ; :: thesis: ( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `2 = ((GoB f) * 1,j) `2 ) )
thus A5: ( 1 <= j & j <= width (GoB f) ) by A3, MATRIX_1:39; :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `2 = ((GoB f) * 1,j) `2
let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg f,k implies p `2 = ((GoB f) * 1,j) `2 )
A6: ( 1 <= i & i <= len (GoB f) ) by A3, MATRIX_1:39;
A7: f /. k in LSeg f,k by A2, TOPREAL1:27;
assume p in LSeg f,k ; :: thesis: p `2 = ((GoB f) * 1,j) `2
hence p `2 = (f /. k) `2 by A1, A7, SPPOL_1:def 2
.= ((GoB f) * 1,j) `2 by A4, A5, A6, GOBOARD5:2 ;
:: thesis: verum

end;

suppose A8: ( not 1 <= k or not k + 1 <= len f ) ; :: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (GoB f) & ( for p being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st p in LSeg f,k holds
p `2 = ((GoB f) * 1,1) `2 ) )
width (GoB f) <> 0 by GOBOARD1:def 5;
hence ( 1 <= 1 & 1 <= width (GoB f) ) by NAT_1:14; :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `2 = ((GoB f) * 1,1) `2
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 5; :: thesis: verum

end;

end;