let f be FinSequence of (); :: thesis: for r being Real
for u being Point of ()
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; :: thesis: for u being Point of ()
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 (); :: thesis: 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; :: thesis: ( 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 ; :: thesis: not f /. m in Ball (u,r)
assume A5: f /. m in Ball (u,r) ; :: thesis: contradiction
per cases ( 1 = m or 1 < m ) by ;
suppose 1 = m ; :: thesis: contradiction
end;
suppose A6: 1 < m ; :: thesis: contradiction
reconsider k = m - 1 as Element of NAT by ;
1 + 1 <= m by ;
then A7: 1 <= m - 1 by XREAL_1:19;
m - 1 <= m by XREAL_1:43;
then A8: k <= (len f) - 1 by ;
then k + 1 <= len f by XREAL_1:19;
then f /. (k + 1) in LSeg (f,k) by ;
then (LSeg (f,k)) /\ (Ball (u,r)) <> {} by ;
then m <= k by A4, A7, A8;
then m + 1 <= m by XREAL_1:19;
hence contradiction by NAT_1:13; :: thesis: verum
end;
end;