let f be non empty FinSequence of (TOP-REAL 2); 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; ( 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
; 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 )
;
suppose A2:
( 1
<= k &
k + 1
<= len f )
;
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 ) )
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
;
( 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;
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);
( 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)
;
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
;
verum end; end;