let V be non empty MetrSpace; :: thesis: ( V is convex implies V is internal )
assume A1: V is convex ; :: thesis: V is internal
let x, y be Element of V; :: according to VECTMETR:def 2 :: thesis: for p, q being Real st p > 0 & q > 0 holds
ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
abs ((dist x,y) - (Sum F)) < q ) )
let p, q be Real; :: thesis: ( p > 0 & q > 0 implies ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
abs ((dist x,y) - (Sum F)) < q ) ) )
assume that
A2: p > 0 and
A3: q > 0 ; :: thesis: ex f being FinSequence of the carrier of V st
( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
abs ((dist x,y) - (Sum F)) < q ) )
consider f being FinSequence of the carrier of V such that
A4: f /. 1 = x and
A5: f /. (len f) = y and
A6: for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p and
A7: for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
dist x,y = Sum F by A1, A2, Th1;
take f ; :: thesis: ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p ) & ( for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
abs ((dist x,y) - (Sum F)) < q ) )
thus ( f /. 1 = x & f /. (len f) = y & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p ) ) by A4, A5, A6; :: thesis: for F being FinSequence of REAL st len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) holds
abs ((dist x,y) - (Sum F)) < q
let F be FinSequence of REAL ; :: thesis: ( len F = (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ) implies abs ((dist x,y) - (Sum F)) < q )
assume that
A8: len F = (len f) - 1 and
A9: for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ; :: thesis: abs ((dist x,y) - (Sum F)) < q
dist x,y = Sum F by A7, A8, A9;
hence abs ((dist x,y) - (Sum F)) < q by A3, ABSVALUE:7; :: thesis: verum