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

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