let V be non empty MetrSpace; :: thesis: ( V is convex implies for x, y being Element of V

for p being Real st p > 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 ) ) )

assume A1: V is convex ; :: thesis: for x, y being Element of V

for p being Real st p > 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 ) )

set A = the carrier of V;

let x, y be Element of V; :: thesis: for p being Real st p > 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 ) )

defpred S_{1}[ set , set , set ] means for a1, a2 being Element of the carrier of V st $1 = [a1,a2] holds

ex b being Element of the carrier of V st

( $2 = [a1,b] & $3 = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) );

A2: for a being Element of [: the carrier of V, the carrier of V:] ex c, d being Element of [: the carrier of V, the carrier of V:] st S_{1}[a,c,d]

A8: dom D = {0,1} * and

A9: D . {} = [x,y] and

A10: for z being Node of D holds S_{1}[D . z,D . (z ^ <*0*>),D . (z ^ <*1*>)]
from BINTREE2:sch 1(A2);

reconsider dD = dom D as full Tree by A8, BINTREE2:def 2;

let p be Real; :: thesis: ( p > 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 ) ) )

assume A11: p > 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 ) )

for p being Real st p > 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 ) ) )

assume A1: V is convex ; :: thesis: for x, y being Element of V

for p being Real st p > 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 ) )

set A = the carrier of V;

let x, y be Element of V; :: thesis: for p being Real st p > 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 ) )

defpred S

ex b being Element of the carrier of V st

( $2 = [a1,b] & $3 = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) );

A2: for a being Element of [: the carrier of V, the carrier of V:] ex c, d being Element of [: the carrier of V, the carrier of V:] st S

proof

consider D being binary DecoratedTree of [: the carrier of V, the carrier of V:] such that
let a be Element of [: the carrier of V, the carrier of V:]; :: thesis: ex c, d being Element of [: the carrier of V, the carrier of V:] st S_{1}[a,c,d]

consider a19, a29 being object such that

A3: ( a19 in the carrier of V & a29 in the carrier of V ) and

A4: a = [a19,a29] by ZFMISC_1:def 2;

reconsider a19 = a19, a29 = a29 as Element of the carrier of V by A3;

consider z being Element of the carrier of V such that

A5: dist (a19,z) = (1 / 2) * (dist (a19,a29)) and

A6: dist (z,a29) = (1 - (1 / 2)) * (dist (a19,a29)) by A1;

take c = [a19,z]; :: thesis: ex d being Element of [: the carrier of V, the carrier of V:] st S_{1}[a,c,d]

take d = [z,a29]; :: thesis: S_{1}[a,c,d]

let a1, a2 be Element of the carrier of V; :: thesis: ( a = [a1,a2] implies ex b being Element of the carrier of V st

( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) ) )

assume A7: a = [a1,a2] ; :: thesis: ex b being Element of the carrier of V st

( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) )

take z ; :: thesis: ( c = [a1,z] & d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )

thus c = [a1,z] by A4, A7, XTUPLE_0:1; :: thesis: ( d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )

thus d = [z,a2] by A4, A7, XTUPLE_0:1; :: thesis: ( dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )

a1 = a19 by A4, A7, XTUPLE_0:1;

hence dist (a1,a2) = 2 * (dist (a1,z)) by A4, A5, A7, XTUPLE_0:1; :: thesis: dist (a1,a2) = 2 * (dist (z,a2))

a2 = a29 by A4, A7, XTUPLE_0:1;

hence dist (a1,a2) = 2 * (dist (z,a2)) by A4, A6, A7, XTUPLE_0:1; :: thesis: verum

end;consider a19, a29 being object such that

A3: ( a19 in the carrier of V & a29 in the carrier of V ) and

A4: a = [a19,a29] by ZFMISC_1:def 2;

reconsider a19 = a19, a29 = a29 as Element of the carrier of V by A3;

consider z being Element of the carrier of V such that

A5: dist (a19,z) = (1 / 2) * (dist (a19,a29)) and

A6: dist (z,a29) = (1 - (1 / 2)) * (dist (a19,a29)) by A1;

take c = [a19,z]; :: thesis: ex d being Element of [: the carrier of V, the carrier of V:] st S

take d = [z,a29]; :: thesis: S

let a1, a2 be Element of the carrier of V; :: thesis: ( a = [a1,a2] implies ex b being Element of the carrier of V st

( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) ) )

assume A7: a = [a1,a2] ; :: thesis: ex b being Element of the carrier of V st

( c = [a1,b] & d = [b,a2] & dist (a1,a2) = 2 * (dist (a1,b)) & dist (a1,a2) = 2 * (dist (b,a2)) )

take z ; :: thesis: ( c = [a1,z] & d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )

thus c = [a1,z] by A4, A7, XTUPLE_0:1; :: thesis: ( d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )

thus d = [z,a2] by A4, A7, XTUPLE_0:1; :: thesis: ( dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )

a1 = a19 by A4, A7, XTUPLE_0:1;

hence dist (a1,a2) = 2 * (dist (a1,z)) by A4, A5, A7, XTUPLE_0:1; :: thesis: dist (a1,a2) = 2 * (dist (z,a2))

a2 = a29 by A4, A7, XTUPLE_0:1;

hence dist (a1,a2) = 2 * (dist (z,a2)) by A4, A6, A7, XTUPLE_0:1; :: thesis: verum

A8: dom D = {0,1} * and

A9: D . {} = [x,y] and

A10: for z being Node of D holds S

reconsider dD = dom D as full Tree by A8, BINTREE2:def 2;

let p be Real; :: thesis: ( p > 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 ) ) )

assume A11: p > 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 ) )

per cases
( dist (x,y) >= p or dist (x,y) < p )
;

end;

suppose
dist (x,y) >= p
; :: 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 ) )

( 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 ) )

then
(dist (x,y)) / p >= 1
by A11, XREAL_1:181;

then log (2,((dist (x,y)) / p)) >= log (2,1) by PRE_FF:10;

then log (2,((dist (x,y)) / p)) >= 0 by POWER:51;

then reconsider n1 = [\(log (2,((dist (x,y)) / p)))/] as Element of NAT by INT_1:53;

defpred S_{2}[ Nat] means for t being Tuple of $1, BOOLEAN st t = 0* $1 holds

(D . ('not' t)) `2 = y;

defpred S_{3}[ Nat] means (D . (0* $1)) `1 = x;

reconsider n = n1 + 1 as non zero Element of NAT ;

reconsider N = 2 to_power n as non zero Element of NAT by POWER:34;

set r = (dist (x,y)) / N;

reconsider FSL = FinSeqLevel (n,dD) as FinSequence of dom D by FINSEQ_2:24;

deffunc H_{1}( Nat) -> Element of [: the carrier of V, the carrier of V:] = D . (FSL /. $1);

consider g being FinSequence of [: the carrier of V, the carrier of V:] such that

A12: len g = N and

A13: for k being Nat st k in dom g holds

g . k = H_{1}(k)
from FINSEQ_2:sch 1();

A14: dom g = Seg N by A12, FINSEQ_1:def 3;

A15: for j being Nat st S_{3}[j] holds

S_{3}[j + 1]
_{3}[ 0 ]
by A9;

A21: for j being Nat holds S_{3}[j]
from NAT_1:sch 2(A20, A15);

2 to_power n > 0 by POWER:34;

then 0 + 1 <= 2 to_power n by NAT_1:13;

then A22: 1 <= len (FinSeqLevel (n,dD)) by BINTREE2:19;

A23: for j being non zero Nat st S_{2}[j] holds

S_{2}[j + 1]
_{2}[1]
_{2}[j]
from NAT_1:sch 10(A31, A23);

deffunc H_{2}( Nat) -> Element of the carrier of V = (g /. $1) `1 ;

consider h being FinSequence of the carrier of V such that

A34: len h = N and

A35: for k being Nat st k in dom h holds

h . k = H_{2}(k)
from FINSEQ_2:sch 1();

A36: dom h = Seg N by A34, FINSEQ_1:def 3;

A37: 1 <= N by NAT_1:14;

then A38: 1 in Seg N by FINSEQ_1:1;

then A39: 1 in dom h by A34, FINSEQ_1:def 3;

take f = h ^ <*y*>; :: 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 ) )

A40: len f = (len h) + (len <*y*>) by FINSEQ_1:22

.= (len h) + 1 by FINSEQ_1:39 ;

1 <= N + 1 by NAT_1:11;

hence f /. 1 = f . 1 by A34, A40, FINSEQ_4:15

.= h . 1 by A39, FINSEQ_1:def 7

.= (g /. 1) `1 by A35, A36, A38

.= (g . 1) `1 by A12, A37, FINSEQ_4:15

.= (D . (FSL /. 1)) `1 by A13, A14, A38

.= (D . ((FinSeqLevel (n,dD)) . 1)) `1 by A22, FINSEQ_4:15

.= (D . (0* n)) `1 by BINTREE2:15

.= x by A21 ;

:: thesis: ( 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 ) )

len f in Seg (len f) by A40, FINSEQ_1:4;

then len f in dom f by FINSEQ_1:def 3;

hence A41: f /. (len f) = (h ^ <*y*>) . ((len h) + 1) by A40, PARTFUN1:def 6

.= y by FINSEQ_1:42 ;

:: thesis: ( ( 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 ) )

A42: for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds

dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N

then log (2,((dist (x,y)) / p)) < n * (log (2,2)) by POWER:52;

then log (2,((dist (x,y)) / p)) < log (2,(2 to_power n)) by POWER:55;

then (dist (x,y)) / p < N by PRE_FF:10;

then ((dist (x,y)) / p) * p < N * p by A11, XREAL_1:68;

then dist (x,y) < N * p by A11, XCMPLX_1:87;

then (dist (x,y)) / N < (N * p) / N by XREAL_1:74;

then (dist (x,y)) / N < (p / N) * N by XCMPLX_1:74;

then (dist (x,y)) / N < p by XCMPLX_1:87;

hence for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds

dist ((f /. i),(f /. (i + 1))) < p by A42; :: 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

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 )

assume that

A117: len F = (len f) - 1 and

A118: 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

A119: rng F = {((dist (x,y)) / N)}

then F = (len F) |-> ((dist (x,y)) / N) by A119, FUNCOP_1:9;

hence Sum F = ((N + 1) - 1) * ((dist (x,y)) / N) by A34, A40, A117, RVSUM_1:80

.= dist (x,y) by XCMPLX_1:87 ;

:: thesis: verum

end;then log (2,((dist (x,y)) / p)) >= log (2,1) by PRE_FF:10;

then log (2,((dist (x,y)) / p)) >= 0 by POWER:51;

then reconsider n1 = [\(log (2,((dist (x,y)) / p)))/] as Element of NAT by INT_1:53;

defpred S

(D . ('not' t)) `2 = y;

defpred S

reconsider n = n1 + 1 as non zero Element of NAT ;

reconsider N = 2 to_power n as non zero Element of NAT by POWER:34;

set r = (dist (x,y)) / N;

reconsider FSL = FinSeqLevel (n,dD) as FinSequence of dom D by FINSEQ_2:24;

deffunc H

consider g being FinSequence of [: the carrier of V, the carrier of V:] such that

A12: len g = N and

A13: for k being Nat st k in dom g holds

g . k = H

A14: dom g = Seg N by A12, FINSEQ_1:def 3;

A15: for j being Nat st S

S

proof

A20:
S
let j be Nat; :: thesis: ( S_{3}[j] implies S_{3}[j + 1] )

assume A16: (D . (0* j)) `1 = x ; :: thesis: S_{3}[j + 1]

reconsider zj = 0* j as Node of D by A8, BINARI_3:4;

consider a, b being object such that

A17: ( a in the carrier of V & b in the carrier of V ) and

A18: D . zj = [a,b] by ZFMISC_1:def 2;

reconsider a1 = a, b1 = b as Element of the carrier of V by A17;

A19: ex z1 being Element of the carrier of V st

( D . (zj ^ <*0*>) = [a1,z1] & D . (zj ^ <*1*>) = [z1,b1] & dist (a1,b1) = 2 * (dist (a1,z1)) & dist (a1,b1) = 2 * (dist (z1,b1)) ) by A10, A18;

thus (D . (0* (j + 1))) `1 = (D . (zj ^ <*0*>)) `1 by FINSEQ_2:60

.= a1 by A19

.= x by A18, A16 ; :: thesis: verum

end;assume A16: (D . (0* j)) `1 = x ; :: thesis: S

reconsider zj = 0* j as Node of D by A8, BINARI_3:4;

consider a, b being object such that

A17: ( a in the carrier of V & b in the carrier of V ) and

A18: D . zj = [a,b] by ZFMISC_1:def 2;

reconsider a1 = a, b1 = b as Element of the carrier of V by A17;

A19: ex z1 being Element of the carrier of V st

( D . (zj ^ <*0*>) = [a1,z1] & D . (zj ^ <*1*>) = [z1,b1] & dist (a1,b1) = 2 * (dist (a1,z1)) & dist (a1,b1) = 2 * (dist (z1,b1)) ) by A10, A18;

thus (D . (0* (j + 1))) `1 = (D . (zj ^ <*0*>)) `1 by FINSEQ_2:60

.= a1 by A19

.= x by A18, A16 ; :: thesis: verum

A21: for j being Nat holds S

2 to_power n > 0 by POWER:34;

then 0 + 1 <= 2 to_power n by NAT_1:13;

then A22: 1 <= len (FinSeqLevel (n,dD)) by BINTREE2:19;

A23: for j being non zero Nat st S

S

proof

A31:
S
let j be non zero Nat; :: thesis: ( S_{2}[j] implies S_{2}[j + 1] )

assume A24: for t being Tuple of j, BOOLEAN st t = 0* j holds

(D . ('not' t)) `2 = y ; :: thesis: S_{2}[j + 1]

let t be Tuple of j + 1, BOOLEAN ; :: thesis: ( t = 0* (j + 1) implies (D . ('not' t)) `2 = y )

consider t1 being Element of j -tuples_on BOOLEAN, dd being Element of BOOLEAN such that

A25: t = t1 ^ <*dd*> by FINSEQ_2:117;

assume A26: t = 0* (j + 1) ; :: thesis: (D . ('not' t)) `2 = y

then t = (0* j) ^ <*0*> by FINSEQ_2:60;

then t1 = 0* j by A25, FINSEQ_2:17;

then A27: (D . ('not' t1)) `2 = y by A24;

dd = t . ((len t1) + 1) by A25, FINSEQ_1:42

.= ((j + 1) |-> 0) . (j + 1) by A26

.= FALSE ;

then 'not' dd = 1 ;

then A28: 'not' t = ('not' t1) ^ <*1*> by A25, BINARI_2:9;

reconsider nt1 = 'not' t1 as Node of D by A8, FINSEQ_1:def 11;

consider a, b being object such that

A29: ( a in the carrier of V & b in the carrier of V ) and

A30: D . nt1 = [a,b] by ZFMISC_1:def 2;

reconsider a1 = a, b1 = b as Element of the carrier of V by A29;

ex b being Element of the carrier of V st

( D . (nt1 ^ <*0*>) = [a1,b] & D . (nt1 ^ <*1*>) = [b,b1] & dist (a1,b1) = 2 * (dist (a1,b)) & dist (a1,b1) = 2 * (dist (b,b1)) ) by A10, A30;

hence (D . ('not' t)) `2 = b1 by A28

.= y by A30, A27 ;

:: thesis: verum

end;assume A24: for t being Tuple of j, BOOLEAN st t = 0* j holds

(D . ('not' t)) `2 = y ; :: thesis: S

let t be Tuple of j + 1, BOOLEAN ; :: thesis: ( t = 0* (j + 1) implies (D . ('not' t)) `2 = y )

consider t1 being Element of j -tuples_on BOOLEAN, dd being Element of BOOLEAN such that

A25: t = t1 ^ <*dd*> by FINSEQ_2:117;

assume A26: t = 0* (j + 1) ; :: thesis: (D . ('not' t)) `2 = y

then t = (0* j) ^ <*0*> by FINSEQ_2:60;

then t1 = 0* j by A25, FINSEQ_2:17;

then A27: (D . ('not' t1)) `2 = y by A24;

dd = t . ((len t1) + 1) by A25, FINSEQ_1:42

.= ((j + 1) |-> 0) . (j + 1) by A26

.= FALSE ;

then 'not' dd = 1 ;

then A28: 'not' t = ('not' t1) ^ <*1*> by A25, BINARI_2:9;

reconsider nt1 = 'not' t1 as Node of D by A8, FINSEQ_1:def 11;

consider a, b being object such that

A29: ( a in the carrier of V & b in the carrier of V ) and

A30: D . nt1 = [a,b] by ZFMISC_1:def 2;

reconsider a1 = a, b1 = b as Element of the carrier of V by A29;

ex b being Element of the carrier of V st

( D . (nt1 ^ <*0*>) = [a1,b] & D . (nt1 ^ <*1*>) = [b,b1] & dist (a1,b1) = 2 * (dist (a1,b)) & dist (a1,b1) = 2 * (dist (b,b1)) ) by A10, A30;

hence (D . ('not' t)) `2 = b1 by A28

.= y by A30, A27 ;

:: thesis: verum

proof

A33:
for j being non zero Nat holds S
reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def 11;

let t be Tuple of 1, BOOLEAN ; :: thesis: ( t = 0* 1 implies (D . ('not' t)) `2 = y )

A32: ex b being Element of the carrier of V st

( D . (pusty ^ <*0*>) = [x,b] & D . (pusty ^ <*1*>) = [b,y] & dist (x,y) = 2 * (dist (x,b)) & dist (x,y) = 2 * (dist (b,y)) ) by A9, A10;

assume t = 0* 1 ; :: thesis: (D . ('not' t)) `2 = y

then t = <*FALSE*> by FINSEQ_2:59;

hence (D . ('not' t)) `2 = (D . (pusty ^ <*1*>)) `2 by BINARI_3:14, FINSEQ_1:34

.= y by A32 ;

:: thesis: verum

end;let t be Tuple of 1, BOOLEAN ; :: thesis: ( t = 0* 1 implies (D . ('not' t)) `2 = y )

A32: ex b being Element of the carrier of V st

( D . (pusty ^ <*0*>) = [x,b] & D . (pusty ^ <*1*>) = [b,y] & dist (x,y) = 2 * (dist (x,b)) & dist (x,y) = 2 * (dist (b,y)) ) by A9, A10;

assume t = 0* 1 ; :: thesis: (D . ('not' t)) `2 = y

then t = <*FALSE*> by FINSEQ_2:59;

hence (D . ('not' t)) `2 = (D . (pusty ^ <*1*>)) `2 by BINARI_3:14, FINSEQ_1:34

.= y by A32 ;

:: thesis: verum

deffunc H

consider h being FinSequence of the carrier of V such that

A34: len h = N and

A35: for k being Nat st k in dom h holds

h . k = H

A36: dom h = Seg N by A34, FINSEQ_1:def 3;

A37: 1 <= N by NAT_1:14;

then A38: 1 in Seg N by FINSEQ_1:1;

then A39: 1 in dom h by A34, FINSEQ_1:def 3;

take f = h ^ <*y*>; :: 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 ) )

A40: len f = (len h) + (len <*y*>) by FINSEQ_1:22

.= (len h) + 1 by FINSEQ_1:39 ;

1 <= N + 1 by NAT_1:11;

hence f /. 1 = f . 1 by A34, A40, FINSEQ_4:15

.= h . 1 by A39, FINSEQ_1:def 7

.= (g /. 1) `1 by A35, A36, A38

.= (g . 1) `1 by A12, A37, FINSEQ_4:15

.= (D . (FSL /. 1)) `1 by A13, A14, A38

.= (D . ((FinSeqLevel (n,dD)) . 1)) `1 by A22, FINSEQ_4:15

.= (D . (0* n)) `1 by BINTREE2:15

.= x by A21 ;

:: thesis: ( 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 ) )

len f in Seg (len f) by A40, FINSEQ_1:4;

then len f in dom f by FINSEQ_1:def 3;

hence A41: f /. (len f) = (h ^ <*y*>) . ((len h) + 1) by A40, PARTFUN1:def 6

.= y by FINSEQ_1:42 ;

:: thesis: ( ( 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 ) )

A42: for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds

dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N

proof

log (2,((dist (x,y)) / p)) < n * 1
by INT_1:29;
0* n in BOOLEAN *
by BINARI_3:4;

then reconsider ze = 0* n as Tuple of n, BOOLEAN by FINSEQ_1:def 11;

reconsider ze = ze as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

defpred S_{4}[ non zero Nat] means for j being non zero Element of NAT st j <= 2 to_power $1 holds

for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ($1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ($1,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power $1);

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (len f) - 1 implies dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N )

assume that

A43: 1 <= i and

A44: i <= (len f) - 1 ; :: thesis: dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N

A45: len FSL = N by BINTREE2:19;

_{4}[l] holds

S_{4}[l + 1]
_{4}[1]
_{4}[l]
from NAT_1:sch 10(A103, A86);

A116: i in Seg (len h) by A40, A43, A44, FINSEQ_1:1;

then i in dom h by FINSEQ_1:def 3;

then f /. i = h /. i by FINSEQ_4:68

.= h . i by A40, A43, A44, FINSEQ_4:15

.= (g /. i) `1 by A34, A35, A36, A116

.= (g . i) `1 by A12, A34, A40, A43, A44, FINSEQ_4:15

.= (D . (FSL /. i)) `1 by A13, A14, A34, A116

.= (D . ((FinSeqLevel (n,dD)) . i)) `1 by A34, A40, A43, A44, A45, FINSEQ_4:15 ;

hence dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N by A34, A40, A43, A44, A46, A115; :: thesis: verum

end;then reconsider ze = 0* n as Tuple of n, BOOLEAN by FINSEQ_1:def 11;

reconsider ze = ze as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

defpred S

for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ($1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ($1,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power $1);

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (len f) - 1 implies dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N )

assume that

A43: 1 <= i and

A44: i <= (len f) - 1 ; :: thesis: dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N

A45: len FSL = N by BINTREE2:19;

A46: now :: thesis: f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2 end;

A86:
for l being non zero Nat st Sper cases
( i < (len f) - 1 or i = (len f) - 1 )
by A44, XXREAL_0:1;

end;

suppose
i < (len f) - 1
; :: thesis: f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2

then
i < (len f) -' 1
by A40, NAT_1:11, XREAL_1:233;

then i + 1 <= (len f) -' 1 by NAT_1:13;

then A47: i + 1 <= (len f) - 1 by A40, NAT_1:11, XREAL_1:233;

then A48: (i + 1) - 1 <= (2 to_power n) - 1 by A34, A40, XREAL_1:9;

defpred S_{5}[ non zero Nat] means for i being Nat st 1 <= i & i <= (2 to_power $1) - 1 holds

(D . ((FinSeqLevel ($1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ($1,dD)) . i)) `2 ;

A49: for n being non zero Nat st S_{5}[n] holds

S_{5}[n + 1]
_{5}[1]
_{5}[n]
from NAT_1:sch 10(A77, A49);

A83: 1 <= 1 + i by NAT_1:11;

then A84: i + 1 in Seg (len h) by A40, A47, FINSEQ_1:1;

then i + 1 in dom h by FINSEQ_1:def 3;

hence f /. (i + 1) = h /. (i + 1) by FINSEQ_4:68

.= h . (i + 1) by A40, A47, A83, FINSEQ_4:15

.= (g /. (i + 1)) `1 by A34, A35, A36, A84

.= (g . (i + 1)) `1 by A12, A34, A40, A47, A83, FINSEQ_4:15

.= (D . (FSL /. (i + 1))) `1 by A13, A14, A34, A84

.= (D . ((FinSeqLevel (n,dD)) . (i + 1))) `1 by A34, A40, A45, A47, A83, FINSEQ_4:15

.= (D . ((FinSeqLevel (n,dD)) . i)) `2 by A43, A48, A82 ;

:: thesis: verum

end;then i + 1 <= (len f) -' 1 by NAT_1:13;

then A47: i + 1 <= (len f) - 1 by A40, NAT_1:11, XREAL_1:233;

then A48: (i + 1) - 1 <= (2 to_power n) - 1 by A34, A40, XREAL_1:9;

defpred S

(D . ((FinSeqLevel ($1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ($1,dD)) . i)) `2 ;

A49: for n being non zero Nat st S

S

proof

A77:
S
let n be non zero Nat; :: thesis: ( S_{5}[n] implies S_{5}[n + 1] )

reconsider nn = n as non zero Element of NAT by ORDINAL1:def 12;

reconsider zb = dD -level n as non empty set by A8, BINTREE2:10;

assume A50: for i being Nat st 1 <= i & i <= (2 to_power n) - 1 holds

(D . ((FinSeqLevel (n,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (n,dD)) . i)) `2 ; :: thesis: S_{5}[n + 1]

let i be Nat; :: thesis: ( 1 <= i & i <= (2 to_power (n + 1)) - 1 implies (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2 )

assume that

A51: 1 <= i and

A52: i <= (2 to_power (n + 1)) - 1 ; :: thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2

reconsider ii = i as Element of NAT by ORDINAL1:def 12;

A53: 1 + 1 <= i + 1 by A51, XREAL_1:6;

then A54: (i + 1) div 2 >= 1 by NAT_2:13;

2 to_power (n + 1) > 0 by POWER:34;

then A55: 2 to_power (n + 1) >= 0 + 1 by NAT_1:13;

then i <= (2 to_power (n + 1)) -' 1 by A52, XREAL_1:233;

then i < ((2 to_power (n + 1)) -' 1) + 1 by NAT_1:13;

then A56: i < ((2 to_power (n + 1)) - 1) + 1 by A55, XREAL_1:233;

then A57: i + 1 <= 2 to_power (n + 1) by NAT_1:13;

then i + 1 <= (2 to_power n) * (2 to_power 1) by POWER:27;

then i + 1 <= (2 to_power n) * 2 by POWER:25;

then A58: ((i + 1) + 1) div 2 <= 2 to_power n by NAT_2:25;

i + 1 <= (i + 1) + 1 by NAT_1:11;

then 2 <= (i + 1) + 1 by A53, XXREAL_0:2;

then ((i + 1) + 1) div 2 >= 1 by NAT_2:13;

then ((i + 1) + 1) div 2 in Seg (2 to_power n) by A58, FINSEQ_1:1;

then ((i + 1) + 1) div 2 in dom (FinSeqLevel (nn,dD)) by BINTREE2:20;

then (FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2) in zb by FINSEQ_2:11;

then reconsider FF = (FinSeqLevel (nn,dD)) . (((i + 1) + 1) div 2) as Tuple of n, BOOLEAN by BINTREE2:5;

reconsider FF = FF as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

reconsider FF1 = FF as Node of D by A8, FINSEQ_1:def 11;

consider a9, b9 being object such that

A59: ( a9 in the carrier of V & b9 in the carrier of V ) and

A60: D . FF1 = [a9,b9] by ZFMISC_1:def 2;

i <= (2 to_power n) * (2 to_power 1) by A56, POWER:27;

then i <= (2 to_power n) * 2 by POWER:25;

then (i + 1) div 2 <= 2 to_power n by NAT_2:25;

then (i + 1) div 2 in Seg (2 to_power n) by A54, FINSEQ_1:1;

then (i + 1) div 2 in dom (FinSeqLevel (nn,dD)) by BINTREE2:20;

then (FinSeqLevel (n,dD)) . ((i + 1) div 2) in zb by FINSEQ_2:11;

then reconsider F = (FinSeqLevel (nn,dD)) . ((i + 1) div 2) as Tuple of n, BOOLEAN by BINTREE2:5;

reconsider F = F as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

reconsider F1 = F as Node of D by A8, FINSEQ_1:def 11;

consider a, b being object such that

A61: ( a in the carrier of V & b in the carrier of V ) and

A62: D . F1 = [a,b] by ZFMISC_1:def 2;

reconsider a1 = a, b1 = b, a19 = a9, b19 = b9 as Element of the carrier of V by A61, A59;

consider d being Element of the carrier of V such that

A63: D . (F1 ^ <*0*>) = [a1,d] and

A64: D . (F1 ^ <*1*>) = [d,b1] and

dist (a1,b1) = 2 * (dist (a1,d)) and

dist (a1,b1) = 2 * (dist (d,b1)) by A10, A62;

consider d9 being Element of the carrier of V such that

A65: D . (FF1 ^ <*0*>) = [a19,d9] and

A66: D . (FF1 ^ <*1*>) = [d9,b19] and

dist (a19,b19) = 2 * (dist (a19,d9)) and

dist (a19,b19) = 2 * (dist (d9,b19)) by A10, A60;

A67: i = (i + 1) - 1

.= (i + 1) -' 1 by NAT_1:11, XREAL_1:233 ;

end;reconsider nn = n as non zero Element of NAT by ORDINAL1:def 12;

reconsider zb = dD -level n as non empty set by A8, BINTREE2:10;

assume A50: for i being Nat st 1 <= i & i <= (2 to_power n) - 1 holds

(D . ((FinSeqLevel (n,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (n,dD)) . i)) `2 ; :: thesis: S

let i be Nat; :: thesis: ( 1 <= i & i <= (2 to_power (n + 1)) - 1 implies (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2 )

assume that

A51: 1 <= i and

A52: i <= (2 to_power (n + 1)) - 1 ; :: thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2

reconsider ii = i as Element of NAT by ORDINAL1:def 12;

A53: 1 + 1 <= i + 1 by A51, XREAL_1:6;

then A54: (i + 1) div 2 >= 1 by NAT_2:13;

2 to_power (n + 1) > 0 by POWER:34;

then A55: 2 to_power (n + 1) >= 0 + 1 by NAT_1:13;

then i <= (2 to_power (n + 1)) -' 1 by A52, XREAL_1:233;

then i < ((2 to_power (n + 1)) -' 1) + 1 by NAT_1:13;

then A56: i < ((2 to_power (n + 1)) - 1) + 1 by A55, XREAL_1:233;

then A57: i + 1 <= 2 to_power (n + 1) by NAT_1:13;

then i + 1 <= (2 to_power n) * (2 to_power 1) by POWER:27;

then i + 1 <= (2 to_power n) * 2 by POWER:25;

then A58: ((i + 1) + 1) div 2 <= 2 to_power n by NAT_2:25;

i + 1 <= (i + 1) + 1 by NAT_1:11;

then 2 <= (i + 1) + 1 by A53, XXREAL_0:2;

then ((i + 1) + 1) div 2 >= 1 by NAT_2:13;

then ((i + 1) + 1) div 2 in Seg (2 to_power n) by A58, FINSEQ_1:1;

then ((i + 1) + 1) div 2 in dom (FinSeqLevel (nn,dD)) by BINTREE2:20;

then (FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2) in zb by FINSEQ_2:11;

then reconsider FF = (FinSeqLevel (nn,dD)) . (((i + 1) + 1) div 2) as Tuple of n, BOOLEAN by BINTREE2:5;

reconsider FF = FF as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

reconsider FF1 = FF as Node of D by A8, FINSEQ_1:def 11;

consider a9, b9 being object such that

A59: ( a9 in the carrier of V & b9 in the carrier of V ) and

A60: D . FF1 = [a9,b9] by ZFMISC_1:def 2;

i <= (2 to_power n) * (2 to_power 1) by A56, POWER:27;

then i <= (2 to_power n) * 2 by POWER:25;

then (i + 1) div 2 <= 2 to_power n by NAT_2:25;

then (i + 1) div 2 in Seg (2 to_power n) by A54, FINSEQ_1:1;

then (i + 1) div 2 in dom (FinSeqLevel (nn,dD)) by BINTREE2:20;

then (FinSeqLevel (n,dD)) . ((i + 1) div 2) in zb by FINSEQ_2:11;

then reconsider F = (FinSeqLevel (nn,dD)) . ((i + 1) div 2) as Tuple of n, BOOLEAN by BINTREE2:5;

reconsider F = F as Element of n -tuples_on BOOLEAN by FINSEQ_2:131;

reconsider F1 = F as Node of D by A8, FINSEQ_1:def 11;

consider a, b being object such that

A61: ( a in the carrier of V & b in the carrier of V ) and

A62: D . F1 = [a,b] by ZFMISC_1:def 2;

reconsider a1 = a, b1 = b, a19 = a9, b19 = b9 as Element of the carrier of V by A61, A59;

consider d being Element of the carrier of V such that

A63: D . (F1 ^ <*0*>) = [a1,d] and

A64: D . (F1 ^ <*1*>) = [d,b1] and

dist (a1,b1) = 2 * (dist (a1,d)) and

dist (a1,b1) = 2 * (dist (d,b1)) by A10, A62;

consider d9 being Element of the carrier of V such that

A65: D . (FF1 ^ <*0*>) = [a19,d9] and

A66: D . (FF1 ^ <*1*>) = [d9,b19] and

dist (a19,b19) = 2 * (dist (a19,d9)) and

dist (a19,b19) = 2 * (dist (d9,b19)) by A10, A60;

A67: i = (i + 1) - 1

.= (i + 1) -' 1 by NAT_1:11, XREAL_1:233 ;

now :: thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 end;

hence
(D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2
; :: thesis: verumper cases
( i is odd or i is even )
;

end;

suppose
i is odd
; :: thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2

then A68:
i mod 2 = 1
by NAT_2:22;

then (i + 1) mod 2 = 0 by A67, NAT_2:18;

then i + 1 is even by NAT_2:21;

then (i + 1) div 2 = ((i + 1) + 1) div 2 by NAT_2:26;

then A69: d = d9 by A63, A65, XTUPLE_0:1;

thus (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 by A57, BINTREE2:24

.= (D . (FF ^ <*1*>)) `1 by A68, NAT_D:21

.= d by A66, A69

.= (D . (F ^ <*0*>)) `2 by A63

.= (D . (F ^ <*((ii + 1) mod 2)*>)) `2 by A67, A68, NAT_2:18

.= (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 by A51, A56, BINTREE2:24 ; :: thesis: verum

end;then (i + 1) mod 2 = 0 by A67, NAT_2:18;

then i + 1 is even by NAT_2:21;

then (i + 1) div 2 = ((i + 1) + 1) div 2 by NAT_2:26;

then A69: d = d9 by A63, A65, XTUPLE_0:1;

thus (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 by A57, BINTREE2:24

.= (D . (FF ^ <*1*>)) `1 by A68, NAT_D:21

.= d by A66, A69

.= (D . (F ^ <*0*>)) `2 by A63

.= (D . (F ^ <*((ii + 1) mod 2)*>)) `2 by A67, A68, NAT_2:18

.= (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 by A51, A56, BINTREE2:24 ; :: thesis: verum

suppose
i is even
; :: thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2

then A70:
i mod 2 = 0
by NAT_2:21;

then A71: 1 = (i -' 1) mod 2 by A51, NAT_2:18

.= ((i -' 1) + (2 * 1)) mod 2 by NAT_D:21

.= (((i -' 1) + 1) + 1) mod 2

.= (i + 1) mod 2 by A51, XREAL_1:235 ;

A72: 1 + (1 + i) >= 1 by NAT_1:11;

(1 + 1) + (i -' 1) = (1 + 1) + (i - 1) by A51, XREAL_1:233

.= ((1 + 1) + i) - 1 ;

then 1 = (((1 + 1) + i) -' 1) mod 2 by A71, A72, XREAL_1:233;

then ((1 + 1) + i) mod 2 = 0 by NAT_2:18;

then (i + 1) + 1 = (2 * (((i + 1) + 1) div 2)) + 0 by NAT_D:2;

then A73: 2 divides (i + 1) + 1 by NAT_D:3;

1 <= (i + 1) + 1 by NAT_1:11;

then (((i + 1) + 1) -' 1) div 2 = (((i + 1) + 1) div 2) - 1 by A73, NAT_2:15;

then (i + 1) div 2 = (((i + 1) + 1) div 2) - 1 by NAT_D:34;

then A74: ((i + 1) div 2) + 1 = ((i + 1) + 1) div 2 ;

then A75: (i + 1) div 2 <= (2 to_power n) - 1 by A58, XREAL_1:19;

A76: a9 = (D . ((FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2))) `1 by A60

.= (D . ((FinSeqLevel (n,dD)) . ((i + 1) div 2))) `2 by A50, A54, A74, A75

.= b by A62 ;

thus (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 by A57, BINTREE2:24

.= (D . (FF ^ <*0*>)) `1 by A70, NAT_D:21

.= a19 by A65

.= (D . (F ^ <*1*>)) `2 by A64, A76

.= (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 by A51, A56, A71, BINTREE2:24 ; :: thesis: verum

end;then A71: 1 = (i -' 1) mod 2 by A51, NAT_2:18

.= ((i -' 1) + (2 * 1)) mod 2 by NAT_D:21

.= (((i -' 1) + 1) + 1) mod 2

.= (i + 1) mod 2 by A51, XREAL_1:235 ;

A72: 1 + (1 + i) >= 1 by NAT_1:11;

(1 + 1) + (i -' 1) = (1 + 1) + (i - 1) by A51, XREAL_1:233

.= ((1 + 1) + i) - 1 ;

then 1 = (((1 + 1) + i) -' 1) mod 2 by A71, A72, XREAL_1:233;

then ((1 + 1) + i) mod 2 = 0 by NAT_2:18;

then (i + 1) + 1 = (2 * (((i + 1) + 1) div 2)) + 0 by NAT_D:2;

then A73: 2 divides (i + 1) + 1 by NAT_D:3;

1 <= (i + 1) + 1 by NAT_1:11;

then (((i + 1) + 1) -' 1) div 2 = (((i + 1) + 1) div 2) - 1 by A73, NAT_2:15;

then (i + 1) div 2 = (((i + 1) + 1) div 2) - 1 by NAT_D:34;

then A74: ((i + 1) div 2) + 1 = ((i + 1) + 1) div 2 ;

then A75: (i + 1) div 2 <= (2 to_power n) - 1 by A58, XREAL_1:19;

A76: a9 = (D . ((FinSeqLevel (n,dD)) . (((i + 1) + 1) div 2))) `1 by A60

.= (D . ((FinSeqLevel (n,dD)) . ((i + 1) div 2))) `2 by A50, A54, A74, A75

.= b by A62 ;

thus (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 by A57, BINTREE2:24

.= (D . (FF ^ <*0*>)) `1 by A70, NAT_D:21

.= a19 by A65

.= (D . (F ^ <*1*>)) `2 by A64, A76

.= (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 by A51, A56, A71, BINTREE2:24 ; :: thesis: verum

proof

A82:
for n being non zero Nat holds S
reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def 11;

let i be Nat; :: thesis: ( 1 <= i & i <= (2 to_power 1) - 1 implies (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2 )

A78: (2 to_power 1) - 1 = (1 + 1) - 1 by POWER:25

.= 1 ;

consider b being Element of the carrier of V such that

A79: D . (pusty ^ <*0*>) = [x,b] and

A80: D . (pusty ^ <*1*>) = [b,y] and

dist (x,y) = 2 * (dist (x,b)) and

dist (x,y) = 2 * (dist (b,y)) by A9, A10;

assume ( 1 <= i & i <= (2 to_power 1) - 1 ) ; :: thesis: (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2

then A81: i = 1 by A78, XXREAL_0:1;

hence (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . <*1*>) `1 by BINTREE2:23

.= (D . (pusty ^ <*1*>)) `1 by FINSEQ_1:34

.= b by A80

.= (D . (pusty ^ <*0*>)) `2 by A79

.= (D . <*0*>) `2 by FINSEQ_1:34

.= (D . ((FinSeqLevel (1,dD)) . i)) `2 by A81, BINTREE2:22 ;

:: thesis: verum

end;let i be Nat; :: thesis: ( 1 <= i & i <= (2 to_power 1) - 1 implies (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2 )

A78: (2 to_power 1) - 1 = (1 + 1) - 1 by POWER:25

.= 1 ;

consider b being Element of the carrier of V such that

A79: D . (pusty ^ <*0*>) = [x,b] and

A80: D . (pusty ^ <*1*>) = [b,y] and

dist (x,y) = 2 * (dist (x,b)) and

dist (x,y) = 2 * (dist (b,y)) by A9, A10;

assume ( 1 <= i & i <= (2 to_power 1) - 1 ) ; :: thesis: (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . ((FinSeqLevel (1,dD)) . i)) `2

then A81: i = 1 by A78, XXREAL_0:1;

hence (D . ((FinSeqLevel (1,dD)) . (i + 1))) `1 = (D . <*1*>) `1 by BINTREE2:23

.= (D . (pusty ^ <*1*>)) `1 by FINSEQ_1:34

.= b by A80

.= (D . (pusty ^ <*0*>)) `2 by A79

.= (D . <*0*>) `2 by FINSEQ_1:34

.= (D . ((FinSeqLevel (1,dD)) . i)) `2 by A81, BINTREE2:22 ;

:: thesis: verum

A83: 1 <= 1 + i by NAT_1:11;

then A84: i + 1 in Seg (len h) by A40, A47, FINSEQ_1:1;

then i + 1 in dom h by FINSEQ_1:def 3;

hence f /. (i + 1) = h /. (i + 1) by FINSEQ_4:68

.= h . (i + 1) by A40, A47, A83, FINSEQ_4:15

.= (g /. (i + 1)) `1 by A34, A35, A36, A84

.= (g . (i + 1)) `1 by A12, A34, A40, A47, A83, FINSEQ_4:15

.= (D . (FSL /. (i + 1))) `1 by A13, A14, A34, A84

.= (D . ((FinSeqLevel (n,dD)) . (i + 1))) `1 by A34, A40, A45, A47, A83, FINSEQ_4:15

.= (D . ((FinSeqLevel (n,dD)) . i)) `2 by A43, A48, A82 ;

:: thesis: verum

S

proof

A103:
S
let l be non zero Nat; :: thesis: ( S_{4}[l] implies S_{4}[l + 1] )

reconsider dDll = dD -level l as non empty set by A8, BINTREE2:10;

reconsider ll = l as non zero Element of NAT by ORDINAL1:def 12;

reconsider dDll1 = dD -level (l + 1) as non empty set by A8, BINTREE2:10;

assume A87: for j being non zero Element of NAT st j <= 2 to_power l holds

for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (l,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (l,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power l) ; :: thesis: S_{4}[l + 1]

let j be non zero Element of NAT ; :: thesis: ( j <= 2 to_power (l + 1) implies for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) )

(j + 1) div 2 <> 0

assume A88: j <= 2 to_power (l + 1) ; :: thesis: for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))

then j <= (2 to_power l) * (2 to_power 1) by POWER:27;

then A89: j <= (2 to_power l) * 2 by POWER:25;

then ( j1 >= 1 & j1 <= 2 to_power l ) by NAT_1:14, NAT_2:25;

then j1 in Seg (2 to_power l) by FINSEQ_1:1;

then (j + 1) div 2 in dom (FinSeqLevel (ll,dD)) by BINTREE2:20;

then (FinSeqLevel (l,dD)) . ((j + 1) div 2) in dDll by FINSEQ_2:11;

then reconsider FSLlprim = (FinSeqLevel (ll,dD)) . ((j + 1) div 2) as Tuple of l, BOOLEAN by BINTREE2:5;

reconsider FSLlprim = FSLlprim as Element of l -tuples_on BOOLEAN by FINSEQ_2:131;

A90: FinSeqLevel ((l + 1),dD) is FinSequence of dom D by FINSEQ_2:24;

j >= 1 by NAT_1:14;

then j in Seg (2 to_power (l + 1)) by A88, FINSEQ_1:1;

then A91: j in dom (FinSeqLevel ((l + 1),dD)) by BINTREE2:20;

then reconsider Fj = (FinSeqLevel ((l + 1),dD)) . j as Element of dom D by A90, FINSEQ_2:11;

(FinSeqLevel ((l + 1),dD)) . j in dDll1 by A91, FINSEQ_2:11;

then reconsider FSLl1 = (FinSeqLevel ((l + 1),dD)) . j as Tuple of l + 1, BOOLEAN by BINTREE2:5;

consider FSLl being Element of l -tuples_on BOOLEAN, d being Element of BOOLEAN such that

A92: FSLl1 = FSLl ^ <*d*> by FINSEQ_2:117;

let DF1, DF2 be Element of V; :: thesis: ( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) )

assume ( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 ) ; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))

then A93: D . Fj = [DF1,DF2] by MCART_1:21;

reconsider NFSLl = FSLl as Node of D by A8, FINSEQ_1:def 11;

consider x1, y1 being object such that

A94: ( x1 in the carrier of V & y1 in the carrier of V ) and

A95: D . NFSLl = [x1,y1] by ZFMISC_1:def 2;

reconsider x1 = x1, y1 = y1 as Element of the carrier of V by A94;

consider b being Element of the carrier of V such that

A96: D . (NFSLl ^ <*0*>) = [x1,b] and

A97: D . (NFSLl ^ <*1*>) = [b,y1] and

A98: dist (x1,y1) = 2 * (dist (x1,b)) and

A99: dist (x1,y1) = 2 * (dist (b,y1)) by A10, A95;

A100: (FinSeqLevel ((ll + 1),dD)) . j = FSLlprim ^ <*((j + 1) mod 2)*> by A88, BINTREE2:24;

then FSLl = FSLlprim by A92, FINSEQ_2:17;

then A101: ( x1 = (D . ((FinSeqLevel (l,dD)) . j1)) `1 & y1 = (D . ((FinSeqLevel (l,dD)) . j1)) `2 ) by A95;

A102: d = (j + 1) mod 2 by A92, A100, FINSEQ_2:17;

end;reconsider dDll = dD -level l as non empty set by A8, BINTREE2:10;

reconsider ll = l as non zero Element of NAT by ORDINAL1:def 12;

reconsider dDll1 = dD -level (l + 1) as non empty set by A8, BINTREE2:10;

assume A87: for j being non zero Element of NAT st j <= 2 to_power l holds

for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (l,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (l,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power l) ; :: thesis: S

let j be non zero Element of NAT ; :: thesis: ( j <= 2 to_power (l + 1) implies for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) )

(j + 1) div 2 <> 0

proof

then reconsider j1 = (j + 1) div 2 as non zero Element of NAT ;
assume
(j + 1) div 2 = 0
; :: thesis: contradiction

then j + 1 < 1 + 1 by NAT_2:12;

then j < 1 by XREAL_1:6;

hence contradiction by NAT_1:14; :: thesis: verum

end;then j + 1 < 1 + 1 by NAT_2:12;

then j < 1 by XREAL_1:6;

hence contradiction by NAT_1:14; :: thesis: verum

assume A88: j <= 2 to_power (l + 1) ; :: thesis: for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))

then j <= (2 to_power l) * (2 to_power 1) by POWER:27;

then A89: j <= (2 to_power l) * 2 by POWER:25;

then ( j1 >= 1 & j1 <= 2 to_power l ) by NAT_1:14, NAT_2:25;

then j1 in Seg (2 to_power l) by FINSEQ_1:1;

then (j + 1) div 2 in dom (FinSeqLevel (ll,dD)) by BINTREE2:20;

then (FinSeqLevel (l,dD)) . ((j + 1) div 2) in dDll by FINSEQ_2:11;

then reconsider FSLlprim = (FinSeqLevel (ll,dD)) . ((j + 1) div 2) as Tuple of l, BOOLEAN by BINTREE2:5;

reconsider FSLlprim = FSLlprim as Element of l -tuples_on BOOLEAN by FINSEQ_2:131;

A90: FinSeqLevel ((l + 1),dD) is FinSequence of dom D by FINSEQ_2:24;

j >= 1 by NAT_1:14;

then j in Seg (2 to_power (l + 1)) by A88, FINSEQ_1:1;

then A91: j in dom (FinSeqLevel ((l + 1),dD)) by BINTREE2:20;

then reconsider Fj = (FinSeqLevel ((l + 1),dD)) . j as Element of dom D by A90, FINSEQ_2:11;

(FinSeqLevel ((l + 1),dD)) . j in dDll1 by A91, FINSEQ_2:11;

then reconsider FSLl1 = (FinSeqLevel ((l + 1),dD)) . j as Tuple of l + 1, BOOLEAN by BINTREE2:5;

consider FSLl being Element of l -tuples_on BOOLEAN, d being Element of BOOLEAN such that

A92: FSLl1 = FSLl ^ <*d*> by FINSEQ_2:117;

let DF1, DF2 be Element of V; :: thesis: ( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) )

assume ( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 ) ; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))

then A93: D . Fj = [DF1,DF2] by MCART_1:21;

reconsider NFSLl = FSLl as Node of D by A8, FINSEQ_1:def 11;

consider x1, y1 being object such that

A94: ( x1 in the carrier of V & y1 in the carrier of V ) and

A95: D . NFSLl = [x1,y1] by ZFMISC_1:def 2;

reconsider x1 = x1, y1 = y1 as Element of the carrier of V by A94;

consider b being Element of the carrier of V such that

A96: D . (NFSLl ^ <*0*>) = [x1,b] and

A97: D . (NFSLl ^ <*1*>) = [b,y1] and

A98: dist (x1,y1) = 2 * (dist (x1,b)) and

A99: dist (x1,y1) = 2 * (dist (b,y1)) by A10, A95;

A100: (FinSeqLevel ((ll + 1),dD)) . j = FSLlprim ^ <*((j + 1) mod 2)*> by A88, BINTREE2:24;

then FSLl = FSLlprim by A92, FINSEQ_2:17;

then A101: ( x1 = (D . ((FinSeqLevel (l,dD)) . j1)) `1 & y1 = (D . ((FinSeqLevel (l,dD)) . j1)) `2 ) by A95;

A102: d = (j + 1) mod 2 by A92, A100, FINSEQ_2:17;

now :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))end;

hence
dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))
; :: thesis: verumper cases
( d = 0 or d = 1 )
by A102, NAT_D:12;

end;

suppose
d = 0
; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))

then
( DF1 = x1 & DF2 = b )
by A93, A92, A96, XTUPLE_0:1;

then 2 * (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2 by A87, A89, A98, A101, NAT_2:25;

hence dist (DF1,DF2) = (dist (x,y)) / ((2 to_power l) * 2) by XCMPLX_1:78

.= (dist (x,y)) / ((2 to_power l) * (2 to_power 1)) by POWER:25

.= (dist (x,y)) / (2 to_power (l + 1)) by POWER:27 ;

:: thesis: verum

end;then 2 * (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2 by A87, A89, A98, A101, NAT_2:25;

hence dist (DF1,DF2) = (dist (x,y)) / ((2 to_power l) * 2) by XCMPLX_1:78

.= (dist (x,y)) / ((2 to_power l) * (2 to_power 1)) by POWER:25

.= (dist (x,y)) / (2 to_power (l + 1)) by POWER:27 ;

:: thesis: verum

suppose
d = 1
; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))

then
( DF1 = b & DF2 = y1 )
by A93, A92, A97, XTUPLE_0:1;

then 2 * (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2 by A87, A89, A99, A101, NAT_2:25;

hence dist (DF1,DF2) = (dist (x,y)) / ((2 to_power l) * 2) by XCMPLX_1:78

.= (dist (x,y)) / ((2 to_power l) * (2 to_power 1)) by POWER:25

.= (dist (x,y)) / (2 to_power (l + 1)) by POWER:27 ;

:: thesis: verum

end;then 2 * (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2 by A87, A89, A99, A101, NAT_2:25;

hence dist (DF1,DF2) = (dist (x,y)) / ((2 to_power l) * 2) by XCMPLX_1:78

.= (dist (x,y)) / ((2 to_power l) * (2 to_power 1)) by POWER:25

.= (dist (x,y)) / (2 to_power (l + 1)) by POWER:27 ;

:: thesis: verum

proof

A115:
for l being non zero Nat holds S
reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def 11;

let j be non zero Element of NAT ; :: thesis: ( j <= 2 to_power 1 implies for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) )

assume A104: j <= 2 to_power 1 ; :: thesis: for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1)

A105: FinSeqLevel (1,dD) is FinSequence of dom D by FINSEQ_2:24;

j >= 1 by NAT_1:14;

then j in Seg (2 to_power 1) by A104, FINSEQ_1:1;

then j in dom (FinSeqLevel (1,dD)) by BINTREE2:20;

then reconsider FSL1j = (FinSeqLevel (1,dD)) . j as Element of dom D by A105, FINSEQ_2:11;

let DF1, DF2 be Element of V; :: thesis: ( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) )

assume A106: ( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 ) ; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1)

( 2 to_power 1 = 2 & j >= 1 ) by NAT_1:14, POWER:25;

then A107: j in Seg 2 by A104, FINSEQ_1:1;

end;let j be non zero Element of NAT ; :: thesis: ( j <= 2 to_power 1 implies for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) )

assume A104: j <= 2 to_power 1 ; :: thesis: for DF1, DF2 being Element of V st DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 holds

dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1)

A105: FinSeqLevel (1,dD) is FinSequence of dom D by FINSEQ_2:24;

j >= 1 by NAT_1:14;

then j in Seg (2 to_power 1) by A104, FINSEQ_1:1;

then j in dom (FinSeqLevel (1,dD)) by BINTREE2:20;

then reconsider FSL1j = (FinSeqLevel (1,dD)) . j as Element of dom D by A105, FINSEQ_2:11;

let DF1, DF2 be Element of V; :: thesis: ( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 implies dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) )

assume A106: ( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 ) ; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1)

( 2 to_power 1 = 2 & j >= 1 ) by NAT_1:14, POWER:25;

then A107: j in Seg 2 by A104, FINSEQ_1:1;

now :: thesis: dist (DF1,DF2) = (dist (x,y)) / 2end;

hence
dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1)
by POWER:25; :: thesis: verumper cases
( j = 1 or j = 2 )
by A107, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A108:
j = 1
; :: thesis: dist (DF1,DF2) = (dist (x,y)) / 2

A109:
ex b being Element of the carrier of V st

( D . (pusty ^ <*0*>) = [x,b] & D . (pusty ^ <*1*>) = [b,y] & dist (x,y) = 2 * (dist (x,b)) & dist (x,y) = 2 * (dist (b,y)) ) by A9, A10;

A110: D . (pusty ^ <*0*>) = D . <*0*> by FINSEQ_1:34

.= D . FSL1j by A108, BINTREE2:22

.= [DF1,DF2] by A106, MCART_1:21 ;

then DF1 = x by A109, XTUPLE_0:1;

hence dist (DF1,DF2) = (dist (x,y)) / 2 by A110, A109, XTUPLE_0:1; :: thesis: verum

end;( D . (pusty ^ <*0*>) = [x,b] & D . (pusty ^ <*1*>) = [b,y] & dist (x,y) = 2 * (dist (x,b)) & dist (x,y) = 2 * (dist (b,y)) ) by A9, A10;

A110: D . (pusty ^ <*0*>) = D . <*0*> by FINSEQ_1:34

.= D . FSL1j by A108, BINTREE2:22

.= [DF1,DF2] by A106, MCART_1:21 ;

then DF1 = x by A109, XTUPLE_0:1;

hence dist (DF1,DF2) = (dist (x,y)) / 2 by A110, A109, XTUPLE_0:1; :: thesis: verum

suppose A111:
j = 2
; :: thesis: dist (DF1,DF2) = (dist (x,y)) / 2

consider b being Element of the carrier of V such that

D . (pusty ^ <*0*>) = [x,b] and

A112: D . (pusty ^ <*1*>) = [b,y] and

dist (x,y) = 2 * (dist (x,b)) and

A113: dist (x,y) = 2 * (dist (b,y)) by A9, A10;

A114: D . (pusty ^ <*1*>) = D . <*1*> by FINSEQ_1:34

.= D . FSL1j by A111, BINTREE2:23

.= [DF1,DF2] by A106, MCART_1:21 ;

then DF1 = b by A112, XTUPLE_0:1;

hence dist (DF1,DF2) = (dist (x,y)) / 2 by A114, A112, A113, XTUPLE_0:1; :: thesis: verum

end;D . (pusty ^ <*0*>) = [x,b] and

A112: D . (pusty ^ <*1*>) = [b,y] and

dist (x,y) = 2 * (dist (x,b)) and

A113: dist (x,y) = 2 * (dist (b,y)) by A9, A10;

A114: D . (pusty ^ <*1*>) = D . <*1*> by FINSEQ_1:34

.= D . FSL1j by A111, BINTREE2:23

.= [DF1,DF2] by A106, MCART_1:21 ;

then DF1 = b by A112, XTUPLE_0:1;

hence dist (DF1,DF2) = (dist (x,y)) / 2 by A114, A112, A113, XTUPLE_0:1; :: thesis: verum

A116: i in Seg (len h) by A40, A43, A44, FINSEQ_1:1;

then i in dom h by FINSEQ_1:def 3;

then f /. i = h /. i by FINSEQ_4:68

.= h . i by A40, A43, A44, FINSEQ_4:15

.= (g /. i) `1 by A34, A35, A36, A116

.= (g . i) `1 by A12, A34, A40, A43, A44, FINSEQ_4:15

.= (D . (FSL /. i)) `1 by A13, A14, A34, A116

.= (D . ((FinSeqLevel (n,dD)) . i)) `1 by A34, A40, A43, A44, A45, FINSEQ_4:15 ;

hence dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N by A34, A40, A43, A44, A46, A115; :: thesis: verum

then log (2,((dist (x,y)) / p)) < n * (log (2,2)) by POWER:52;

then log (2,((dist (x,y)) / p)) < log (2,(2 to_power n)) by POWER:55;

then (dist (x,y)) / p < N by PRE_FF:10;

then ((dist (x,y)) / p) * p < N * p by A11, XREAL_1:68;

then dist (x,y) < N * p by A11, XCMPLX_1:87;

then (dist (x,y)) / N < (N * p) / N by XREAL_1:74;

then (dist (x,y)) / N < (p / N) * N by XCMPLX_1:74;

then (dist (x,y)) / N < p by XCMPLX_1:87;

hence for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds

dist ((f /. i),(f /. (i + 1))) < p by A42; :: 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

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 )

assume that

A117: len F = (len f) - 1 and

A118: 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

A119: rng F = {((dist (x,y)) / N)}

proof

dom F = Seg (len F)
by FINSEQ_1:def 3;
thus
rng F c= {((dist (x,y)) / N)}
:: according to XBOOLE_0:def 10 :: thesis: {((dist (x,y)) / N)} c= rng F

assume a in {((dist (x,y)) / N)} ; :: thesis: a in rng F

then a = (dist (x,y)) / N by TARSKI:def 1;

then A124: a = dist ((f /. 1),(f /. (1 + 1))) by A34, A40, A37, A42

.= F /. 1 by A34, A40, A37, A117, A118

.= F . 1 by A34, A40, A37, A117, FINSEQ_4:15 ;

1 in Seg (len F) by A34, A40, A37, A117, FINSEQ_1:1;

then 1 in dom F by FINSEQ_1:def 3;

hence a in rng F by A124, FUNCT_1:def 3; :: thesis: verum

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {((dist (x,y)) / N)} or a in rng F )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng F or a in {((dist (x,y)) / N)} )

assume a in rng F ; :: thesis: a in {((dist (x,y)) / N)}

then consider c being object such that

A120: c in dom F and

A121: F . c = a by FUNCT_1:def 3;

c in Seg (len F) by A120, FINSEQ_1:def 3;

then c in { t where t is Nat : ( 1 <= t & t <= len F ) } by FINSEQ_1:def 1;

then consider c1 being Nat such that

A122: c1 = c and

A123: ( 1 <= c1 & c1 <= len F ) ;

reconsider c1 = c1 as Element of NAT by ORDINAL1:def 12;

a = F /. c1 by A121, A122, A123, FINSEQ_4:15

.= dist ((f /. c1),(f /. (c1 + 1))) by A118, A123

.= (dist (x,y)) / N by A42, A117, A123 ;

hence a in {((dist (x,y)) / N)} by TARSKI:def 1; :: thesis: verum

end;assume a in rng F ; :: thesis: a in {((dist (x,y)) / N)}

then consider c being object such that

A120: c in dom F and

A121: F . c = a by FUNCT_1:def 3;

c in Seg (len F) by A120, FINSEQ_1:def 3;

then c in { t where t is Nat : ( 1 <= t & t <= len F ) } by FINSEQ_1:def 1;

then consider c1 being Nat such that

A122: c1 = c and

A123: ( 1 <= c1 & c1 <= len F ) ;

reconsider c1 = c1 as Element of NAT by ORDINAL1:def 12;

a = F /. c1 by A121, A122, A123, FINSEQ_4:15

.= dist ((f /. c1),(f /. (c1 + 1))) by A118, A123

.= (dist (x,y)) / N by A42, A117, A123 ;

hence a in {((dist (x,y)) / N)} by TARSKI:def 1; :: thesis: verum

assume a in {((dist (x,y)) / N)} ; :: thesis: a in rng F

then a = (dist (x,y)) / N by TARSKI:def 1;

then A124: a = dist ((f /. 1),(f /. (1 + 1))) by A34, A40, A37, A42

.= F /. 1 by A34, A40, A37, A117, A118

.= F . 1 by A34, A40, A37, A117, FINSEQ_4:15 ;

1 in Seg (len F) by A34, A40, A37, A117, FINSEQ_1:1;

then 1 in dom F by FINSEQ_1:def 3;

hence a in rng F by A124, FUNCT_1:def 3; :: thesis: verum

then F = (len F) |-> ((dist (x,y)) / N) by A119, FUNCOP_1:9;

hence Sum F = ((N + 1) - 1) * ((dist (x,y)) / N) by A34, A40, A117, RVSUM_1:80

.= dist (x,y) by XCMPLX_1:87 ;

:: thesis: verum

suppose A125:
dist (x,y) < p
; :: 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 ) )

( 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 ) )

take f = <*x,y*>; :: 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 ) )

thus A126: f /. 1 = x by FINSEQ_4:17; :: thesis: ( 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 ) )

len f = 2 by FINSEQ_1:44;

hence f /. (len f) = y by FINSEQ_4:17; :: thesis: ( ( 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 ) )

A127: (len f) - 1 = (1 + 1) - 1 by FINSEQ_1:44

.= 1 ;

thus for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds

dist ((f /. i),(f /. (i + 1))) < p :: 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

F /. i = dist ((f /. i),(f /. (i + 1))) ) implies dist (x,y) = Sum F )

assume that

A128: len F = (len f) - 1 and

A129: 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

reconsider dxy = dist (x,y) as Element of REAL by XREAL_0:def 1;

1 <= len F by A127, A128;

then 1 in dom F by FINSEQ_3:25;

then F /. 1 = F . 1 by PARTFUN1:def 6;

then F . 1 = dist ((f /. 1),(f /. (1 + 1))) by A127, A128, A129

.= dist (x,y) by A126, FINSEQ_4:17 ;

then F = <*dxy*> by A127, A128, FINSEQ_5:14;

then Sum F = dxy by FINSOP_1:11;

hence dist (x,y) = Sum F ; :: thesis: verum

end;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 ) )

thus A126: f /. 1 = x by FINSEQ_4:17; :: thesis: ( 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 ) )

len f = 2 by FINSEQ_1:44;

hence f /. (len f) = y by FINSEQ_4:17; :: thesis: ( ( 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 ) )

A127: (len f) - 1 = (1 + 1) - 1 by FINSEQ_1:44

.= 1 ;

thus for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds

dist ((f /. i),(f /. (i + 1))) < p :: 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

proof

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
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (len f) - 1 implies dist ((f /. i),(f /. (i + 1))) < p )

assume ( 1 <= i & i <= (len f) - 1 ) ; :: thesis: dist ((f /. i),(f /. (i + 1))) < p

then i in Seg 1 by A127, FINSEQ_1:1;

then i = 1 by FINSEQ_1:2, TARSKI:def 1;

hence dist ((f /. i),(f /. (i + 1))) < p by A125, A126, FINSEQ_4:17; :: thesis: verum

end;assume ( 1 <= i & i <= (len f) - 1 ) ; :: thesis: dist ((f /. i),(f /. (i + 1))) < p

then i in Seg 1 by A127, FINSEQ_1:1;

then i = 1 by FINSEQ_1:2, TARSKI:def 1;

hence dist ((f /. i),(f /. (i + 1))) < p by A125, A126, FINSEQ_4:17; :: thesis: verum

F /. i = dist ((f /. i),(f /. (i + 1))) ) implies dist (x,y) = Sum F )

assume that

A128: len F = (len f) - 1 and

A129: 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

reconsider dxy = dist (x,y) as Element of REAL by XREAL_0:def 1;

1 <= len F by A127, A128;

then 1 in dom F by FINSEQ_3:25;

then F /. 1 = F . 1 by PARTFUN1:def 6;

then F . 1 = dist ((f /. 1),(f /. (1 + 1))) by A127, A128, A129

.= dist (x,y) by A126, FINSEQ_4:17 ;

then F = <*dxy*> by A127, A128, FINSEQ_5:14;

then Sum F = dxy by FINSOP_1:11;

hence dist (x,y) = Sum F ; :: thesis: verum