let f be FinSequence of (TOP-REAL 2); for r being Real
for u being Point of (Euclid 2)
for m being Nat st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds
m <= i ) holds
not f /. m in Ball (u,r)
let r be Real; for u being Point of (Euclid 2)
for m being Nat st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds
m <= i ) holds
not f /. m in Ball (u,r)
let u be Point of (Euclid 2); for m being Nat st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds
m <= i ) holds
not f /. m in Ball (u,r)
let m be Nat; ( not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds
m <= i ) implies not f /. m in Ball (u,r) )
assume that
A1:
not f /. 1 in Ball (u,r)
and
A2:
1 <= m
and
A3:
m <= (len f) - 1
and
A4:
for i being Nat st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds
m <= i
; not f /. m in Ball (u,r)
assume A5:
f /. m in Ball (u,r)
; contradiction
per cases
( 1 = m or 1 < m )
by A2, XXREAL_0:1;
suppose
1
= m
;
contradictionhence
contradiction
by A1, A5;
verum end; suppose A6:
1
< m
;
contradictionreconsider k =
m - 1 as
Element of
NAT by A6, INT_1:5;
1
+ 1
<= m
by A6, NAT_1:13;
then A7:
1
<= m - 1
by XREAL_1:19;
m - 1
<= m
by XREAL_1:43;
then A8:
k <= (len f) - 1
by A3, XXREAL_0:2;
then
k + 1
<= len f
by XREAL_1:19;
then
f /. (k + 1) in LSeg (
f,
k)
by A7, TOPREAL1:21;
then
(LSeg (f,k)) /\ (Ball (u,r)) <> {}
by A5, XBOOLE_0:def 4;
then
m <= k
by A4, A7, A8;
then
m + 1
<= m
by XREAL_1:19;
hence
contradiction
by NAT_1:13;
verum end; end;