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
|.((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
|.((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
|.((dist (x,y)) - (Sum F)).| < q ) )
consider f being FinSequence of the carrier of V such that
A4: ( 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 ) ) and
A5: 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
|.((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; :: 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
|.((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 |.((dist (x,y)) - (Sum F)).| < q )
assume ( 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))) ) ) ; :: thesis: |.((dist (x,y)) - (Sum F)).| < q
then dist (x,y) = Sum F by A5;
hence |.((dist (x,y)) - (Sum F)).| < q by A3, ABSVALUE:2; :: thesis: verum