let q be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2)
for r being real number
for u being Point of (Euclid 2)
for m being Element of NAT st f is being_S-Seq & not f /. 1 in Ball u,r & q in Ball u,r & f /. (len f) in LSeg f,m & 1 <= m & m + 1 <= len f & LSeg f,m meets Ball u,r holds
m + 1 = len f
let f be FinSequence of (TOP-REAL 2); :: thesis: for r being real number
for u being Point of (Euclid 2)
for m being Element of NAT st f is being_S-Seq & not f /. 1 in Ball u,r & q in Ball u,r & f /. (len f) in LSeg f,m & 1 <= m & m + 1 <= len f & LSeg f,m meets Ball u,r holds
m + 1 = len f
let r be real number ; :: thesis: for u being Point of (Euclid 2)
for m being Element of NAT st f is being_S-Seq & not f /. 1 in Ball u,r & q in Ball u,r & f /. (len f) in LSeg f,m & 1 <= m & m + 1 <= len f & LSeg f,m meets Ball u,r holds
m + 1 = len f
let u be Point of (Euclid 2); :: thesis: for m being Element of NAT st f is being_S-Seq & not f /. 1 in Ball u,r & q in Ball u,r & f /. (len f) in LSeg f,m & 1 <= m & m + 1 <= len f & LSeg f,m meets Ball u,r holds
m + 1 = len f
let m be Element of NAT ; :: thesis: ( f is being_S-Seq & not f /. 1 in Ball u,r & q in Ball u,r & f /. (len f) in LSeg f,m & 1 <= m & m + 1 <= len f & LSeg f,m meets Ball u,r implies m + 1 = len f )
assume A1:
( f is being_S-Seq & not f /. 1 in Ball u,r & q in Ball u,r & f /. (len f) in LSeg f,m & 1 <= m & m + 1 <= len f & (LSeg f,m) /\ (Ball u,r) <> {} )
; :: according to XBOOLE_0:def 7 :: thesis: m + 1 = len f
then A2:
len f >= 2
by TOPREAL1:def 10;
then A3:
1 <= len f
by XXREAL_0:2;
reconsider k = (len f) - 1 as Element of NAT by A2, INT_1:18, XXREAL_0:2;
A4:
k + 1 = len f
;
set q = f /. (len f);
A5:
f is s.n.c.
by A1, TOPREAL1:def 10;
A6:
f is unfolded
by A1, TOPREAL1:def 10;
assume
m + 1 <> len f
; :: thesis: contradiction
then A7:
m + 1 <= k
by A1, A4, NAT_1:8;
A8:
(m + 1) + 1 = m + (1 + 1)
;
A9:
f is one-to-one
by A1, TOPREAL1:def 10;
A10:
len f in dom f
by A3, FINSEQ_3:27;
per cases
( m + 1 = k or m + 1 < k )
by A7, XXREAL_0:1;
suppose A11:
m + 1
= k
;
:: thesis: contradictionthen A12:
(LSeg f,m) /\ (LSeg f,(m + 1)) = {(f /. (m + 1))}
by A1, A6, A8, TOPREAL1:def 8;
A13:
(
(m + 1) + 1
<= len f & 1
<= m + 1 &
m + 1
<= len f )
by A4, A11, NAT_1:11;
then
f /. (m + 2) in LSeg f,
(m + 1)
by TOPREAL1:27;
then
f /. (len f) in {(f /. (m + 1))}
by A1, A11, A12, XBOOLE_0:def 4;
then A14:
f /. (len f) = f /. (m + 1)
by TARSKI:def 1;
m + 1
in dom f
by A13, FINSEQ_3:27;
then
len f = (len f) - 1
by A9, A10, A11, A14, PARTFUN2:17;
hence
contradiction
;
:: thesis: verum end; suppose
m + 1
< k
;
:: thesis: contradictionthen
LSeg f,
m misses LSeg f,
k
by A5, TOPREAL1:def 9;
then A15:
(LSeg f,m) /\ (LSeg f,k) = {}
by XBOOLE_0:def 7;
A16:
k + 1
= len f
;
(1 + 1) - 1
= 1
;
then
1
<= k
by A2, XREAL_1:15;
then
f /. (len f) in LSeg f,
k
by A16, TOPREAL1:27;
hence
contradiction
by A1, A15, XBOOLE_0:def 4;
:: thesis: verum end;