let V be non empty MetrSpace; :: thesis:
assume A1: V is convex ; :: thesis:
set A = the carrier of V;
let x, y be Element of V; :: thesis:
defpred S₁[ 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₁[a,c,d]

proof

let a be Element of [: the carrier of V, the carrier of V:]; :: thesis:
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:
take d = [z,a29]; :: thesis:
let a1, a2 be Element of the carrier of V; :: thesis:
assume A7: a = [a1,a2] ; :: thesis:
take z ; :: thesis:
thus c = [a1,z] by A4, A7, XTUPLE_0:1; :: thesis:
thus d = [z,a2] by A4, A7, XTUPLE_0:1; :: thesis:
a1 = a19 by A4, A7, XTUPLE_0:1;
hence dist (a1,a2) = 2 * (dist (a1,z)) by A4, A5, A7, XTUPLE_0:1; :: thesis:
a2 = a29 by A4, A7, XTUPLE_0:1;
hence dist (a1,a2) = 2 * (dist (z,a2)) by A4, A6, A7, XTUPLE_0:1; :: thesis:

end;

consider D being binary DecoratedTree of [: the carrier of V, the carrier of V:] such that
A8: dom D = {0,1} * and
A9: D . {} = [x,y] and
A10: for z being Node of D holds S₁[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:
assume A11: p > 0 ; :: thesis:

per cases ;

suppose dist (x,y) >= p ; :: thesis:

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₂[ Nat] means for t being Tuple of $1, BOOLEAN st t = 0* $1 holds
(D . ('not' t)) `2 = y;
defpred S₃[ 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₁( 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₁(k) from FINSEQ_2:sch 1();
A14: dom g = Seg N by A12, FINSEQ_1:def 3;
A15: for j being Nat st S₃[j] holds
S₃[j + 1]

proof

let j be Nat; :: thesis:
assume A16: (D . (0* j)) `1 = x ; :: thesis:
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:

end;

A20: S₃[ 0 ] by A9;
A21: for j being Nat holds S₃[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₂[j] holds
S₂[j + 1]

proof

let j be non zero Nat; :: thesis:
assume A24: for t being Tuple of j, BOOLEAN st t = 0* j holds
(D . ('not' t)) `2 = y ; :: thesis:
let t be Tuple of j + 1, BOOLEAN ; :: thesis:
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:
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:

end;

A31: S₂[1]

proof

reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def 11;
let t be Tuple of 1, BOOLEAN ; :: thesis:
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:
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:

end;

A33: for j being non zero Nat holds S₂[j] from NAT_1:sch 10(A31, A23);
deffunc H₂( 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₂(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:
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:
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:
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

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₄[ 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:
assume that
A43: 1 <= i and
A44: i <= (len f) - 1 ; :: thesis:
A45: len FSL = N by BINTREE2:19;

A46: now :: thesis:

per cases by A44, XXREAL_0:1;

suppose i < (len f) - 1 ; :: thesis:

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₅[ 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₅[n] holds
S₅[n + 1]

proof

let n be non zero Nat; :: thesis:
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:
let i be Nat; :: thesis:
assume that
A51: 1 <= i and
A52: i <= (2 to_power (n + 1)) - 1 ; :: thesis:
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:

per cases ;

suppose i is odd ; :: thesis:

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:

end;

suppose i is even ; :: thesis:

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:

end;

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

end;

A77: S₅[1]

proof

reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def 11;
let i be Nat; :: thesis:
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:
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:

end;

A82: for n being non zero Nat holds S₅[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:

end;

suppose A85: i = (len f) - 1 ; :: thesis:

hence f /. (i + 1) = (D . ('not' ze)) `2 by A33, A41
.= (D . ((FinSeqLevel (n,dD)) . i)) `2 by A34, A40, A85, BINTREE2:16 ;
:: thesis:

end;

A86: for l being non zero Nat st S₄[l] holds
S₄[l + 1]

proof

let l be non zero Nat; :: thesis:
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:
let j be non zero Element of NAT ; :: thesis:
(j + 1) div 2 <> 0

proof

assume (j + 1) div 2 = 0 ; :: thesis:
then j + 1 < 1 + 1 by NAT_2:12;
then j < 1 by XREAL_1:6;
hence contradiction by NAT_1:14; :: thesis:

end;

then reconsider j1 = (j + 1) div 2 as non zero Element of NAT ;
assume A88: j <= 2 to_power (l + 1) ; :: thesis:
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:
assume ( DF1 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel ((l + 1),dD)) . j)) `2 ) ; :: thesis:
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:

per cases by A102, NAT_D:12;

suppose d = 0 ; :: thesis:

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:

end;

suppose d = 1 ; :: thesis:

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:

end;

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

end;

A103: S₄[1]

proof

reconsider pusty = <*> {0,1} as Node of D by A8, FINSEQ_1:def 11;
let j be non zero Element of NAT ; :: thesis:
assume A104: j <= 2 to_power 1 ; :: thesis:
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:
assume A106: ( DF1 = (D . ((FinSeqLevel (1,dD)) . j)) `1 & DF2 = (D . ((FinSeqLevel (1,dD)) . j)) `2 ) ; :: thesis:
( 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:

per cases by A107, FINSEQ_1:2, TARSKI:def 2;

suppose A108: j = 1 ; :: thesis:

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:

end;

suppose A111: j = 2 ; :: thesis:

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:

end;

hence dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) by POWER:25; :: thesis:

end;

A115: for l being non zero Nat holds S₄[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:

end;

log (2,((dist (x,y)) / p)) < n * 1 by INT_1:29;
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:
let F be FinSequence of REAL ; :: thesis:
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:
A119: rng F = {((dist (x,y)) / N)}

proof

thus rng F c= {((dist (x,y)) / N)} :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng F ; :: thesis:
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:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in {((dist (x,y)) / N)} ; :: thesis:
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:

end;

dom F = Seg (len F) by FINSEQ_1:def 3;
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:

end;

suppose A125: dist (x,y) < p ; :: thesis:

take f = <*x,y*>; :: thesis:
thus A126: f /. 1 = x by FINSEQ_4:17; :: thesis:
len f = 2 by FINSEQ_1:44;
hence f /. (len f) = y by FINSEQ_4:17; :: thesis:
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:

proof

let i be Element of NAT ; :: thesis:
assume ( 1 <= i & i <= (len f) - 1 ) ; :: thesis:
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:

end;

let F be FinSequence of REAL ; :: thesis:
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:
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:

end;