let V be non empty MetrSpace; :: thesis:
assume A1: V is convex ; :: thesis:
let x, y be Element of V; :: thesis:
let p be Real; :: thesis:
assume A2: p > 0 ; :: thesis:
set A = the carrier of V;
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) );
A3: 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 a1', a2' being set such that
A4: a1' in the carrier of V and
A5: a2' in the carrier of V and
A6: a = [a1',a2'] by ZFMISC_1:def 2;
reconsider a1' = a1', a2' = a2' as Element of the carrier of V by A4, A5;
consider z being Element of the carrier of V such that
A7: dist a1',z = (1 / 2) * (dist a1',a2') and
A8: dist z,a2' = (1 - (1 / 2)) * (dist a1',a2') by A1, Def1;
take c = [a1',z]; :: thesis:
take d = [z,a2']; :: thesis:
let a1, a2 be Element of the carrier of V; :: thesis:
assume A9: a = [a1,a2] ; :: thesis:
then A10: ( a1 = a1' & a2 = a2' ) by A6, ZFMISC_1:33;
take z ; :: thesis:
thus c = [a1,z] by A6, A9, ZFMISC_1:33; :: thesis:
thus d = [z,a2] by A6, A9, ZFMISC_1:33; :: thesis:
thus dist a1,a2 = 2 * (dist a1,z) by A7, A10; :: thesis:
thus dist a1,a2 = 2 * (dist z,a2) by A8, A10; :: thesis:

end;

consider D being binary DecoratedTree of such that
A11: dom D = {0 ,1} * and
A12: D . {} = [x,y] and
A13: for z being Node of D holds S₁[D . z,D . (z ^ <*0 *>),D . (z ^ <*1*>)] from BINTREE2:sch 1(A3);
reconsider dD = dom D as full Tree by A11, BINTREE2:def 2;

per cases ;

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

then (dist x,y) / p >= 1 by A2, XREAL_1:183;
then log 2,((dist x,y) / p) >= log 2,1 by PRE_FF:12;
then log 2,((dist x,y) / p) >= 0 by POWER:59;
then reconsider n1 = [\(log 2,((dist x,y) / p))/] as Element of NAT by INT_1:80;
reconsider n = n1 + 1 as non empty Element of NAT ;
A14: 2 to_power n > 0 by POWER:39;
reconsider N = 2 to_power n as non empty Element of NAT by POWER:39;
set r = (dist x,y) / N;
log 2,((dist x,y) / p) < n * 1 by INT_1:52;
then log 2,((dist x,y) / p) < n * (log 2,2) by POWER:60;
then log 2,((dist x,y) / p) < log 2,(2 to_power n) by POWER:63;
then (dist x,y) / p < N by PRE_FF:12;
then ((dist x,y) / p) * p < N * p by A2, XREAL_1:70;
then dist x,y < N * p by A2, XCMPLX_1:88;
then (dist x,y) / N < (N * p) / N by XREAL_1:76;
then (dist x,y) / N < (p / N) * N by XCMPLX_1:75;
then A15: (dist x,y) / N < p by XCMPLX_1:88;
reconsider FSL = FinSeqLevel n,dD as FinSequence of dom D ;
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
A16: len g = N and
A17: for k being Nat st k in dom g holds
g . k = H₁(k) from FINSEQ_2:sch 1();
A18: dom g = Seg N by A16, FINSEQ_1:def 3;
deffunc H₂( Nat) -> Element of the carrier of V = (g /. $1) `1 ;
consider h being FinSequence of the carrier of V such that
A19: len h = N and
A20: for k being Nat st k in dom h holds
h . k = H₂(k) from FINSEQ_2:sch 1();
A21: dom h = Seg N by A19, FINSEQ_1:def 3;
take f = h ^ <*y*>; :: thesis:
defpred S₂[ Element of NAT ] means (D . (0* $1)) `1 = x;
(D . (0* 0 )) `1 = [x,y] `1 by A12;
then A22: S₂[ 0 ] by MCART_1:7;
A23: for j being Element of NAT st S₂[j] holds
S₂[j + 1]

proof

let j be Element of NAT ; :: thesis:
reconsider zj = 0* j as Node of D by A11, BINARI_3:5;
consider a, b being set such that
A24: a in the carrier of V and
A25: b in the carrier of V and
A26: D . zj = [a,b] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b as Element of the carrier of V by A24, A25;
consider z1 being Element of the carrier of V such that
A27: D . (zj ^ <*0 *>) = [a1,z1] and
D . (zj ^ <*1*>) = [z1,b1] and
dist a1,b1 = 2 * (dist a1,z1) and
dist a1,b1 = 2 * (dist z1,b1) by A13, A26;
assume A28: (D . (0* j)) `1 = x ; :: thesis:
thus (D . (0* (j + 1))) `1 = (D . (zj ^ <*0 *>)) `1 by FINSEQ_2:74
.= a1 by A27, MCART_1:7
.= x by A26, A28, MCART_1:7 ; :: thesis:

end;

A29: for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A22, A23);
defpred S₃[ Nat] means for t being Tuple of $1,BOOLEAN st t = 0* $1 holds
(D . ('not' t)) `2 = y;
A30: S₃[1]

proof

let t be Tuple of 1,BOOLEAN ; :: thesis:
reconsider pusty = <*> {0 ,1} as Node of D by A11, FINSEQ_1:def 11;
consider b being Element of the carrier of V such that
D . (pusty ^ <*0 *>) = [x,b] and
A31: D . (pusty ^ <*1*>) = [b,y] and
dist x,y = 2 * (dist x,b) and
dist x,y = 2 * (dist b,y) by A12, A13;
assume t = 0* 1 ; :: thesis:
then t = <*FALSE *> by FINSEQ_2:73;
hence (D . ('not' t)) `2 = (D . (pusty ^ <*1*>)) `2 by BINARI_3:15, FINSEQ_1:47
.= y by A31, MCART_1:7 ;
:: thesis:

end;

A32: for j being non empty Nat st S₃[j] holds
S₃[j + 1]

proof

let j be non empty Nat; :: thesis:
assume A33: 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:
assume A34: t = 0* (j + 1) ; :: thesis:
consider t1 being Tuple of j,BOOLEAN , dd being Element of BOOLEAN such that
A35: t = t1 ^ <*dd*> by FINSEQ_2:137;
dd = t . ((len t1) + 1) by A35, FINSEQ_1:59
.= ((j + 1) |-> 0 ) . (j + 1) by A34, FINSEQ_1:def 18
.= FALSE by FINSEQ_1:6, FUNCOP_1:13 ;
then 'not' dd = 1 ;
then A36: 'not' t = ('not' t1) ^ <*1*> by A35, BINARI_2:11;
reconsider nt1 = 'not' t1 as Node of D by A11, FINSEQ_1:def 11;
consider a, b being set such that
A37: a in the carrier of V and
A38: b in the carrier of V and
A39: D . nt1 = [a,b] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b as Element of the carrier of V by A37, A38;
consider b being Element of the carrier of V such that
D . (nt1 ^ <*0 *>) = [a1,b] and
A40: D . (nt1 ^ <*1*>) = [b,b1] and
dist a1,b1 = 2 * (dist a1,b) and
dist a1,b1 = 2 * (dist b,b1) by A13, A39;
t = (0* j) ^ <*0 *> by A34, FINSEQ_2:74;
then t1 = 0* j by A35, FINSEQ_2:20;
then A41: (D . ('not' t1)) `2 = y by A33;
thus (D . ('not' t)) `2 = b1 by A36, A40, MCART_1:7
.= y by A39, A41, MCART_1:7 ; :: thesis:

end;

A42: for j being non empty Nat holds S₃[j] from NAT_1:sch 10(A30, A32);
A43: len f = (len h) + (len <*y*>) by FINSEQ_1:35
.= (len h) + 1 by FINSEQ_1:56 ;
A44: 1 <= N by NAT_1:14;
then A45: 1 in Seg N by FINSEQ_1:3;
then A46: 1 in dom h by A19, FINSEQ_1:def 3;
0 + 1 <= 2 to_power n by A14, NAT_1:13;
then A47: 1 <= len (FinSeqLevel n,dD) by BINTREE2:19;
1 <= N + 1 by NAT_1:11;
hence f /. 1 = f . 1 by A19, A43, FINSEQ_4:24
.= h . 1 by A46, FINSEQ_1:def 7
.= (g /. 1) `1 by A20, A45, A21
.= (g . 1) `1 by A16, A44, FINSEQ_4:24
.= (D . (FSL /. 1)) `1 by A17, A45, A18
.= (D . ((FinSeqLevel n,dD) . 1)) `1 by A47, FINSEQ_4:24
.= (D . (0* n)) `1 by BINTREE2:15
.= x by A29 ;
:: thesis:
len f in Seg (len f) by A43, FINSEQ_1:6;
then len f in dom f by FINSEQ_1:def 3;
hence A48: f /. (len f) = (h ^ <*y*>) . ((len h) + 1) by A43, PARTFUN1:def 8
.= y by FINSEQ_1:59 ;
:: thesis:
A49: 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

let i be Element of NAT ; :: thesis:
assume that
A50: 1 <= i and
A51: i <= (len f) - 1 ; :: thesis:
A52: len FSL = N by BINTREE2:19;
A53: i in Seg (len h) by A43, A50, A51, FINSEQ_1:3;
then i in dom h by FINSEQ_1:def 3;
then A54: f /. i = h /. i by FINSEQ_4:83
.= h . i by A43, A50, A51, FINSEQ_4:24
.= (g /. i) `1 by A19, A20, A53, A21
.= (g . i) `1 by A16, A19, A43, A50, A51, FINSEQ_4:24
.= (D . (FSL /. i)) `1 by A17, A19, A53, A18
.= (D . ((FinSeqLevel n,dD) . i)) `1 by A19, A43, A50, A51, A52, FINSEQ_4:24 ;
0* n in BOOLEAN * by BINARI_3:5;
then A55: 0* n is FinSequence of BOOLEAN by FINSEQ_1:def 11;
len (0* n) = n by FINSEQ_1:def 18;
then reconsider ze = 0* n as Tuple of n,BOOLEAN by A55, FINSEQ_2:110;

A56: now

per cases by A51, XXREAL_0:1;

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

then i < (len f) -' 1 by A43, NAT_1:11, XREAL_1:235;
then i + 1 <= (len f) -' 1 by NAT_1:13;
then A57: i + 1 <= (len f) - 1 by A43, NAT_1:11, XREAL_1:235;
then A58: (i + 1) - 1 <= (2 to_power n) - 1 by A19, A43, XREAL_1:11;
defpred S₄[ non empty 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 ;
A59: S₄[1]

proof

let i be Nat; :: thesis:
assume that
A60: 1 <= i and
A61: i <= (2 to_power 1) - 1 ; :: thesis:
(2 to_power 1) - 1 = (1 + 1) - 1 by POWER:30
.= 1 ;
then A62: i = 1 by A60, A61, XXREAL_0:1;
reconsider pusty = <*> {0 ,1} as Node of D by A11, FINSEQ_1:def 11;
consider b being Element of the carrier of V such that
A63: D . (pusty ^ <*0 *>) = [x,b] and
A64: D . (pusty ^ <*1*>) = [b,y] and
dist x,y = 2 * (dist x,b) and
dist x,y = 2 * (dist b,y) by A12, A13;
thus (D . ((FinSeqLevel 1,dD) . (i + 1))) `1 = (D . <*1*>) `1 by A62, BINTREE2:23
.= (D . (pusty ^ <*1*>)) `1 by FINSEQ_1:47
.= b by A64, MCART_1:7
.= (D . (pusty ^ <*0 *>)) `2 by A63, MCART_1:7
.= (D . <*0 *>) `2 by FINSEQ_1:47
.= (D . ((FinSeqLevel 1,dD) . i)) `2 by A62, BINTREE2:22 ; :: thesis:

end;

A65: for n being non empty Nat st S₄[n] holds
S₄[n + 1]

proof

let n be non empty Nat; :: thesis:
assume A66: 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
A67: 1 <= i and
A68: i <= (2 to_power (n + 1)) - 1 ; :: thesis:
2 to_power (n + 1) > 0 by POWER:39;
then A69: 2 to_power (n + 1) >= 0 + 1 by NAT_1:13;
then i <= (2 to_power (n + 1)) -' 1 by A68, XREAL_1:235;
then i < ((2 to_power (n + 1)) -' 1) + 1 by NAT_1:13;
then A70: i < ((2 to_power (n + 1)) - 1) + 1 by A69, XREAL_1:235;
then A71: i + 1 <= 2 to_power (n + 1) by NAT_1:13;
reconsider nn = n as non empty Element of NAT by ORDINAL1:def 13;
i <= (2 to_power n) * (2 to_power 1) by A70, POWER:32;
then i <= (2 to_power n) * 2 by POWER:30;
then A72: (i + 1) div 2 <= 2 to_power n by NAT_2:27;
A73: 1 + 1 <= i + 1 by A67, XREAL_1:8;
then A74: (i + 1) div 2 >= 1 by NAT_2:15;
then (i + 1) div 2 in Seg (2 to_power n) by A72, FINSEQ_1:3;
then A75: (i + 1) div 2 in dom (FinSeqLevel nn,dD) by BINTREE2:20;
reconsider zb = dD -level n as non empty set by A11, BINTREE2:10;
(FinSeqLevel n,dD) . ((i + 1) div 2) in zb by A75, FINSEQ_2:13;
then reconsider F = (FinSeqLevel nn,dD) . ((i + 1) div 2) as Tuple of n,BOOLEAN by BINTREE2:5;
reconsider F1 = F as Node of D by A11, FINSEQ_1:def 11;
i + 1 <= (2 to_power n) * (2 to_power 1) by A71, POWER:32;
then i + 1 <= (2 to_power n) * 2 by POWER:30;
then A76: ((i + 1) + 1) div 2 <= 2 to_power n by NAT_2:27;
i + 1 <= (i + 1) + 1 by NAT_1:11;
then 2 <= (i + 1) + 1 by A73, XXREAL_0:2;
then ((i + 1) + 1) div 2 >= 1 by NAT_2:15;
then ((i + 1) + 1) div 2 in Seg (2 to_power n) by A76, FINSEQ_1:3;
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:13;
then reconsider FF = (FinSeqLevel nn,dD) . (((i + 1) + 1) div 2) as Tuple of n,BOOLEAN by BINTREE2:5;
reconsider FF1 = FF as Node of D by A11, FINSEQ_1:def 11;
consider a, b being set such that
A77: a in the carrier of V and
A78: b in the carrier of V and
A79: D . F1 = [a,b] by ZFMISC_1:def 2;
consider a', b' being set such that
A80: a' in the carrier of V and
A81: b' in the carrier of V and
A82: D . FF1 = [a',b'] by ZFMISC_1:def 2;
reconsider a1 = a, b1 = b, a1' = a', b1' = b' as Element of the carrier of V by A77, A78, A80, A81;
consider d being Element of the carrier of V such that
A83: D . (F1 ^ <*0 *>) = [a1,d] and
A84: D . (F1 ^ <*1*>) = [d,b1] and
dist a1,b1 = 2 * (dist a1,d) and
dist a1,b1 = 2 * (dist d,b1) by A13, A79;
consider d' being Element of the carrier of V such that
A85: D . (FF1 ^ <*0 *>) = [a1',d'] and
A86: D . (FF1 ^ <*1*>) = [d',b1'] and
dist a1',b1' = 2 * (dist a1',d') and
dist a1',b1' = 2 * (dist d',b1') by A13, A82;
A87: i = (i + 1) - 1
.= (i + 1) -' 1 by NAT_1:11, XREAL_1:235 ;
reconsider ii = i as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose not i is even ; :: thesis:

then A88: i mod 2 = 1 by NAT_2:24;
then (i + 1) mod 2 = 0 by A87, NAT_2:20;
then i + 1 is even by NAT_2:23;
then (i + 1) div 2 = ((i + 1) + 1) div 2 by NAT_2:28;
then A89: d = d' by A83, A85, ZFMISC_1:33;
thus (D . ((FinSeqLevel (n + 1),dD) . (i + 1))) `1 = (D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 by A71, BINTREE2:24
.= (D . (FF ^ <*1*>)) `1 by A88, NAT_D:21
.= d by A86, A89, MCART_1:7
.= (D . (F ^ <*0 *>)) `2 by A83, MCART_1:7
.= (D . (F ^ <*((ii + 1) mod 2)*>)) `2 by A87, A88, NAT_2:20
.= (D . ((FinSeqLevel (n + 1),dD) . ii)) `2 by A67, A70, BINTREE2:24 ; :: thesis:

end;

suppose i is even ; :: thesis:

then A90: i mod 2 = 0 by NAT_2:23;
then A91: 1 = (i -' 1) mod 2 by A67, NAT_2:20
.= ((i -' 1) + (2 * 1)) mod 2 by NAT_D:21
.= (((i -' 1) + 1) + 1) mod 2
.= (i + 1) mod 2 by A67, XREAL_1:237 ;
A92: 1 + (1 + i) >= 1 by NAT_1:11;
(1 + 1) + (i -' 1) = (1 + 1) + (i - 1) by A67, XREAL_1:235
.= ((1 + 1) + i) - 1 ;
then 1 = (((1 + 1) + i) -' 1) mod 2 by A91, A92, XREAL_1:235;
then ((1 + 1) + i) mod 2 = 0 by NAT_2:20;
then (i + 1) + 1 = (2 * (((i + 1) + 1) div 2)) + 0 by NAT_D:2;
then A93: 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 A93, NAT_2:17;
then (i + 1) div 2 = (((i + 1) + 1) div 2) - 1 by NAT_D:34;
then A94: ((i + 1) div 2) + 1 = ((i + 1) + 1) div 2 ;
then A95: (i + 1) div 2 <= (2 to_power n) - 1 by A76, XREAL_1:21;
A96: a' = (D . ((FinSeqLevel n,dD) . (((i + 1) + 1) div 2))) `1 by A82, MCART_1:7
.= (D . ((FinSeqLevel n,dD) . ((i + 1) div 2))) `2 by A66, A74, A94, A95
.= b by A79, MCART_1:7 ;
thus (D . ((FinSeqLevel (n + 1),dD) . (i + 1))) `1 = (D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 by A71, BINTREE2:24
.= (D . (FF ^ <*0 *>)) `1 by A90, NAT_D:21
.= a1' by A85, MCART_1:7
.= (D . (F ^ <*1*>)) `2 by A84, A96, MCART_1:7
.= (D . ((FinSeqLevel (n + 1),dD) . ii)) `2 by A67, A70, A91, BINTREE2:24 ; :: thesis:

end;

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

end;

A97: for n being non empty Nat holds S₄[n] from NAT_1:sch 10(A59, A65);
A98: 1 <= 1 + i by NAT_1:11;
then A99: i + 1 in Seg (len h) by A43, A57, FINSEQ_1:3;
then i + 1 in dom h by FINSEQ_1:def 3;
hence f /. (i + 1) = h /. (i + 1) by FINSEQ_4:83
.= h . (i + 1) by A43, A57, A98, FINSEQ_4:24
.= (g /. (i + 1)) `1 by A19, A20, A99, A21
.= (g . (i + 1)) `1 by A16, A19, A43, A57, A98, FINSEQ_4:24
.= (D . (FSL /. (i + 1))) `1 by A17, A19, A99, A18
.= (D . ((FinSeqLevel n,dD) . (i + 1))) `1 by A19, A43, A52, A57, A98, FINSEQ_4:24
.= (D . ((FinSeqLevel n,dD) . i)) `2 by A50, A58, A97 ;
:: thesis:

end;

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

hence f /. (i + 1) = (D . ('not' ze)) `2 by A42, A48
.= (D . ((FinSeqLevel n,dD) . i)) `2 by A19, A43, A100, BINTREE2:16 ;
:: thesis:

end;

A101: i >= 0 + 1 by A50;
defpred S₄[ non empty Nat] means for j being non empty 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);
A102: S₄[1]

proof

let j be non empty Element of NAT ; :: thesis:
A103: 2 to_power 1 = 2 by POWER:30;
A104: j >= 1 by NAT_1:14;
assume A105: j <= 2 to_power 1 ; :: thesis:
then A106: j in Seg 2 by A103, A104, FINSEQ_1:3;
let DF1, DF2 be Element of V; :: thesis:
assume that
A107: DF1 = (D . ((FinSeqLevel 1,dD) . j)) `1 and
A108: DF2 = (D . ((FinSeqLevel 1,dD) . j)) `2 ; :: thesis:
reconsider pusty = <*> {0 ,1} as Node of D by A11, FINSEQ_1:def 11;
j >= 1 by NAT_1:14;
then j in Seg (2 to_power 1) by A105, FINSEQ_1:3;
then j in dom (FinSeqLevel 1,dD) by BINTREE2:20;
then reconsider FSL1j = (FinSeqLevel 1,dD) . j as Element of dom D by FINSEQ_2:13;

now

per cases by A106, FINSEQ_1:4, TARSKI:def 2;

suppose A109: j = 1 ; :: thesis:

A110: D . (pusty ^ <*0 *>) = D . <*0 *> by FINSEQ_1:47
.= D . FSL1j by A109, BINTREE2:22
.= [DF1,DF2] by A107, A108, MCART_1:23 ;
consider b being Element of the carrier of V such that
A111: D . (pusty ^ <*0 *>) = [x,b] and
D . (pusty ^ <*1*>) = [b,y] and
A112: dist x,y = 2 * (dist x,b) and
dist x,y = 2 * (dist b,y) by A12, A13;
( DF1 = x & DF2 = b ) by A110, A111, ZFMISC_1:33;
hence dist DF1,DF2 = (dist x,y) / 2 by A112; :: thesis:

end;

suppose A113: j = 2 ; :: thesis:

A114: D . (pusty ^ <*1*>) = D . <*1*> by FINSEQ_1:47
.= D . FSL1j by A113, BINTREE2:23
.= [DF1,DF2] by A107, A108, MCART_1:23 ;
consider b being Element of the carrier of V such that
D . (pusty ^ <*0 *>) = [x,b] and
A115: D . (pusty ^ <*1*>) = [b,y] and
dist x,y = 2 * (dist x,b) and
A116: dist x,y = 2 * (dist b,y) by A12, A13;
( DF1 = b & DF2 = y ) by A114, A115, ZFMISC_1:33;
hence dist DF1,DF2 = (dist x,y) / 2 by A116; :: thesis:

end;

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

end;

A117: for l being non empty Nat st S₄[l] holds
S₄[l + 1]

proof

let l be non empty Nat; :: thesis:
assume A118: for j being non empty 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 empty Element of NAT ; :: thesis:
assume A119: j <= 2 to_power (l + 1) ; :: thesis:
let DF1, DF2 be Element of V; :: thesis:
assume that
A120: DF1 = (D . ((FinSeqLevel (l + 1),dD) . j)) `1 and
A121: DF2 = (D . ((FinSeqLevel (l + 1),dD) . j)) `2 ; :: thesis:
(j + 1) div 2 <> 0

proof

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

end;

then reconsider j1 = (j + 1) div 2 as non empty Element of NAT ;
A122: j1 >= 1 by NAT_1:14;
reconsider ll = l as non empty Element of NAT by ORDINAL1:def 13;
j <= (2 to_power l) * (2 to_power 1) by A119, POWER:32;
then A123: j <= (2 to_power l) * 2 by POWER:30;
then j1 <= 2 to_power l by NAT_2:27;
then j1 in Seg (2 to_power l) by A122, FINSEQ_1:3;
then A124: (j + 1) div 2 in dom (FinSeqLevel ll,dD) by BINTREE2:20;
j >= 1 by NAT_1:14;
then j in Seg (2 to_power (l + 1)) by A119, FINSEQ_1:3;
then A125: j in dom (FinSeqLevel (l + 1),dD) by BINTREE2:20;
reconsider dDll1 = dD -level (l + 1) as non empty set by A11, BINTREE2:10;
(FinSeqLevel (l + 1),dD) . j in dDll1 by A125, FINSEQ_2:13;
then reconsider FSLl1 = (FinSeqLevel (l + 1),dD) . j as Tuple of (l + 1),BOOLEAN by BINTREE2:5;
reconsider Fj = (FinSeqLevel (l + 1),dD) . j as Element of dom D by A125, FINSEQ_2:13;
A126: D . Fj = [DF1,DF2] by A120, A121, MCART_1:23;
consider FSLl being Tuple of l,BOOLEAN , d being Element of BOOLEAN such that
A127: FSLl1 = FSLl ^ <*d*> by FINSEQ_2:137;
reconsider NFSLl = FSLl as Node of D by A11, FINSEQ_1:def 11;
consider x1, y1 being set such that
A128: x1 in the carrier of V and
A129: y1 in the carrier of V and
A130: D . NFSLl = [x1,y1] by ZFMISC_1:def 2;
reconsider x1 = x1, y1 = y1 as Element of the carrier of V by A128, A129;
consider b being Element of the carrier of V such that
A131: D . (NFSLl ^ <*0 *>) = [x1,b] and
A132: D . (NFSLl ^ <*1*>) = [b,y1] and
A133: dist x1,y1 = 2 * (dist x1,b) and
A134: dist x1,y1 = 2 * (dist b,y1) by A13, A130;
reconsider dDll = dD -level l as non empty set by A11, BINTREE2:10;
(FinSeqLevel l,dD) . ((j + 1) div 2) in dDll by A124, FINSEQ_2:13;
then reconsider FSLlprim = (FinSeqLevel ll,dD) . ((j + 1) div 2) as Tuple of l,BOOLEAN by BINTREE2:5;
(FinSeqLevel (ll + 1),dD) . j = FSLlprim ^ <*((j + 1) mod 2)*> by A119, BINTREE2:24;
then A135: ( FSLl = FSLlprim & d = (j + 1) mod 2 ) by A127, FINSEQ_2:20;
then A136: ( x1 = (D . ((FinSeqLevel l,dD) . j1)) `1 & y1 = (D . ((FinSeqLevel l,dD) . j1)) `2 ) by A130, MCART_1:7;

now

per cases by A135, NAT_D:12;

suppose d = 0 ; :: thesis:

then ( DF1 = x1 & DF2 = b ) by A126, A127, A131, ZFMISC_1:33;
then 2 * (dist DF1,DF2) = (((dist x,y) / (2 to_power l)) / 2) * 2 by A118, A123, A133, A136, NAT_2:27;
hence dist DF1,DF2 = (dist x,y) / ((2 to_power l) * 2) by XCMPLX_1:79
.= (dist x,y) / ((2 to_power l) * (2 to_power 1)) by POWER:30
.= (dist x,y) / (2 to_power (l + 1)) by POWER:32 ;
:: thesis:

end;

suppose d = 1 ; :: thesis:

then ( DF1 = b & DF2 = y1 ) by A126, A127, A132, ZFMISC_1:33;
then 2 * (dist DF1,DF2) = (((dist x,y) / (2 to_power l)) / 2) * 2 by A118, A123, A134, A136, NAT_2:27;
hence dist DF1,DF2 = (dist x,y) / ((2 to_power l) * 2) by XCMPLX_1:79
.= (dist x,y) / ((2 to_power l) * (2 to_power 1)) by POWER:30
.= (dist x,y) / (2 to_power (l + 1)) by POWER:32 ;
:: thesis:

end;

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

end;

for l being non empty Nat holds S₄[l] from NAT_1:sch 10(A102, A117);
hence dist (f /. i),(f /. (i + 1)) = (dist x,y) / N by A19, A43, A51, A54, A56, A101; :: thesis:

end;

hence for i being Element of NAT st 1 <= i & i <= (len f) - 1 holds
dist (f /. i),(f /. (i + 1)) < p by A15; :: thesis:
let F be FinSequence of REAL ; :: thesis:
assume that
A137: len F = (len f) - 1 and
A138: for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ; :: thesis:
A139: dom F = Seg (len F) by FINSEQ_1:def 3;
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 set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng F ; :: thesis:
then consider c being set such that
A140: c in dom F and
A141: F . c = a by FUNCT_1:def 5;
c in Seg (len F) by A140, FINSEQ_1:def 3;
then c in { t where t is Element of NAT : ( 1 <= t & t <= len F ) } by FINSEQ_1:def 1;
then consider c1 being Element of NAT such that
A142: c1 = c and
A143: 1 <= c1 and
A144: c1 <= len F ;
a = F /. c1 by A141, A142, A143, A144, FINSEQ_4:24
.= dist (f /. c1),(f /. (c1 + 1)) by A138, A143, A144
.= (dist x,y) / N by A49, A137, A143, A144 ;
hence a in {((dist x,y) / N)} by TARSKI:def 1; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in {((dist x,y) / N)} ; :: thesis:
then A145: a = (dist x,y) / N by TARSKI:def 1;
1 in Seg (len F) by A19, A43, A44, A137, FINSEQ_1:3;
then A146: 1 in dom F by FINSEQ_1:def 3;
a = dist (f /. 1),(f /. (1 + 1)) by A19, A43, A44, A49, A145
.= F /. 1 by A19, A43, A44, A137, A138
.= F . 1 by A19, A43, A44, A137, FINSEQ_4:24 ;
hence a in rng F by A146, FUNCT_1:def 5; :: thesis:

end;

then F = (len F) |-> ((dist x,y) / N) by A139, FUNCOP_1:15;
hence Sum F = ((N + 1) - 1) * ((dist x,y) / N) by A19, A43, A137, RVSUM_1:110
.= dist x,y by XCMPLX_1:88 ;
:: thesis:

end;

suppose A147: dist x,y < p ; :: thesis:

take f = <*x,y*>; :: thesis:
thus A148: f /. 1 = x by FINSEQ_4:26; :: thesis:
len f = 2 by FINSEQ_1:61;
hence f /. (len f) = y by FINSEQ_4:26; :: thesis:
A149: (len f) - 1 = (1 + 1) - 1 by FINSEQ_1:61
.= 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 that
A150: 1 <= i and
A151: i <= (len f) - 1 ; :: thesis:
i in Seg 1 by A149, A150, A151, FINSEQ_1:3;
then i = 1 by FINSEQ_1:4, TARSKI:def 1;
hence dist (f /. i),(f /. (i + 1)) < p by A147, A148, FINSEQ_4:26; :: thesis:

end;

let F be FinSequence of REAL ; :: thesis:
assume that
A152: len F = (len f) - 1 and
A153: for i being Element of NAT st 1 <= i & i <= len F holds
F /. i = dist (f /. i),(f /. (i + 1)) ; :: thesis:
F /. 1 = dist (f /. 1),(f /. (1 + 1)) by A149, A152, A153
.= dist x,y by A148, FINSEQ_4:26 ;
then F = <*(dist x,y)*> by A149, A152, FINSEQ_5:15;
hence dist x,y = Sum F by FINSOP_1:12; :: thesis:

end;