let f be FinSequence of (TOP-REAL 2); :: thesis:
let r be real number ; :: thesis:
let u be Point of (Euclid 2); :: thesis:
let m be Element of NAT ; :: thesis:
assume A1: ( not f /. 1 in Ball u,r & 1 <= m & m <= (len f) - 1 & (LSeg f,m) /\ (Ball u,r) <> {} & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 & (LSeg f,i) /\ (Ball u,r) <> {} holds
m <= i ) ) ; :: according to XBOOLE_0:def 7 :: thesis:
assume A2: f /. m in Ball u,r ; :: thesis:

per cases by A1, XXREAL_0:1;

suppose 1 = m ; :: thesis:

hence contradiction by A1, A2; :: thesis:

end;

suppose A3: 1 < m ; :: thesis:

then 1 + 1 <= m by NAT_1:13;
then A4: 1 <= m - 1 by XREAL_1:21;
reconsider k = m - 1 as Element of NAT by A3, INT_1:18;
m - 1 <= m by XREAL_1:45;
then A5: k <= (len f) - 1 by A1, XXREAL_0:2;
then k + 1 <= len f by XREAL_1:21;
then f /. (k + 1) in LSeg f,k by A4, TOPREAL1:27;
then (LSeg f,k) /\ (Ball u,r) <> {} by A2, XBOOLE_0:def 4;
then m <= k by A1, A4, A5;
then m + 1 <= m by XREAL_1:21;
hence contradiction by NAT_1:13; :: thesis:

end;