let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for k being Element of NAT st LSeg f,k is vertical holds
ex i being Element of 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 Element of NAT ; :: thesis: ( LSeg f,k is vertical implies ex i being Element of 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 Element of 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 )
;
:: thesis: ex i being Element of 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: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
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_1:39;
:: thesis: for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `1 = ((GoB f) * i,1) `1 let p be
Point of
(TOP-REAL 2);
:: thesis: ( p in LSeg f,k implies p `1 = ((GoB f) * i,1) `1 )A6:
( 1
<= j &
j <= width (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 `1 = ((GoB f) * i,1) `1 hence p `1 =
(f /. k) `1
by A1, A7, SPPOL_1:def 3
.=
((GoB f) * i,1) `1
by A4, A5, A6, GOBOARD5:3
;
:: thesis: verum end;