let f be FinSequence of (TOP-REAL 2); :: thesis: 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; :: thesis: 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); :: 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

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; :: thesis: 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); :: 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 A2, XXREAL_0:1;

end;

suppose A6:
1 < m
; :: thesis: contradiction

reconsider 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; :: thesis: verum

end;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; :: thesis: verum