let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for k being Nat st LSeg (f,k) is vertical holds

ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

let k be Nat; :: thesis: ( LSeg (f,k) is vertical implies ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) ) )

assume A1: LSeg (f,k) is vertical ; :: thesis: ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

let k be Nat; :: thesis: ( LSeg (f,k) is vertical implies ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) ) )

assume A1: LSeg (f,k) is vertical ; :: thesis: ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

per cases
( ( 1 <= k & k + 1 <= len f ) or not 1 <= k or not k + 1 <= len f )
;

end;

suppose A2:
( 1 <= k & k + 1 <= len f )
; :: thesis: ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

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 i ; :: thesis: ( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

thus A5: ( 1 <= i & i <= len (GoB f) ) by A3, MATRIX_0:32; :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1

A6: f /. k in LSeg (f,k) by A2, TOPREAL1:21;

let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (f,k) implies p `1 = ((GoB f) * (i,1)) `1 )

A7: ( 1 <= j & j <= width (GoB f) ) by A3, MATRIX_0:32;

assume p in LSeg (f,k) ; :: thesis: p `1 = ((GoB f) * (i,1)) `1

hence p `1 = (f /. k) `1 by A1, A6, SPPOL_1:def 3

.= ((GoB f) * (i,1)) `1 by A4, A5, A7, GOBOARD5:2 ;

:: thesis: verum

end;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 i ; :: thesis: ( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

thus A5: ( 1 <= i & i <= len (GoB f) ) by A3, MATRIX_0:32; :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1

A6: f /. k in LSeg (f,k) by A2, TOPREAL1:21;

let p be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (f,k) implies p `1 = ((GoB f) * (i,1)) `1 )

A7: ( 1 <= j & j <= width (GoB f) ) by A3, MATRIX_0:32;

assume p in LSeg (f,k) ; :: thesis: p `1 = ((GoB f) * (i,1)) `1

hence p `1 = (f /. k) `1 by A1, A6, SPPOL_1:def 3

.= ((GoB f) * (i,1)) `1 by A4, A5, A7, GOBOARD5:2 ;

:: thesis: verum

suppose A8:
( not 1 <= k or not k + 1 <= len f )
; :: thesis: ex i being Nat st

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

( 1 <= i & i <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i,1)) `1 ) )

take
1
; :: thesis: ( 1 <= 1 & 1 <= len (GoB f) & ( for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (1,1)) `1 ) )

0 <> len (GoB f) by MATRIX_0:def 10;

hence ( 1 <= 1 & 1 <= len (GoB f) ) by NAT_1:14; :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (1,1)) `1

thus for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (1,1)) `1 by A8, TOPREAL1:def 3; :: thesis: verum

end;p `1 = ((GoB f) * (1,1)) `1 ) )

0 <> len (GoB f) by MATRIX_0:def 10;

hence ( 1 <= 1 & 1 <= len (GoB f) ) by NAT_1:14; :: thesis: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (1,1)) `1

thus for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (1,1)) `1 by A8, TOPREAL1:def 3; :: thesis: verum