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 S1[ 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 S1[a,c,d]
proof
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 S1[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 S1[a,c,d]
take d = [z,a29]; :: thesis: S1[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 ; :: thesis: ( d = [z,a2] & dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )
thus d = [z,a2] by ; :: thesis: ( dist (a1,a2) = 2 * (dist (a1,z)) & dist (a1,a2) = 2 * (dist (z,a2)) )
a1 = a19 by ;
hence dist (a1,a2) = 2 * (dist (a1,z)) by ; :: thesis: dist (a1,a2) = 2 * (dist (z,a2))
a2 = a29 by ;
hence dist (a1,a2) = 2 * (dist (z,a2)) by ; :: thesis: verum
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 S1[D . z,D . (),D . (z ^ <*1*>)] from reconsider dD = dom D as full Tree by ;
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 ) ;
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 ) )

then (dist (x,y)) / p >= 1 by ;
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 S2[ Nat] means for t being Tuple of \$1, BOOLEAN st t = 0* \$1 holds
(D . ()) `2 = y;
defpred S3[ 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 H1( 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 = H1(k) from A14: dom g = Seg N by ;
A15: for j being Nat st S3[j] holds
S3[j + 1]
proof
let j be Nat; :: thesis: ( S3[j] implies S3[j + 1] )
assume A16: (D . (0* j)) `1 = x ; :: thesis: S3[j + 1]
reconsider zj = 0* j as Node of D by ;
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 ^ ) = [a1,z1] & D . (zj ^ <*1*>) = [z1,b1] & dist (a1,b1) = 2 * (dist (a1,z1)) & dist (a1,b1) = 2 * (dist (z1,b1)) ) by ;
thus (D . (0* (j + 1))) `1 = (D . (zj ^ )) `1 by FINSEQ_2:60
.= a1 by A19
.= x by ; :: thesis: verum
end;
A20: S3[ 0 ] by A9;
A21: for j being Nat holds S3[j] from 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 S2[j] holds
S2[j + 1]
proof
let j be non zero Nat; :: thesis: ( S2[j] implies S2[j + 1] )
assume A24: for t being Tuple of j, BOOLEAN st t = 0* j holds
(D . ()) `2 = y ; :: thesis: S2[j + 1]
let t be Tuple of j + 1, BOOLEAN ; :: thesis: ( t = 0* (j + 1) implies (D . ()) `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 . ()) `2 = y
then t = (0* j) ^ by FINSEQ_2:60;
then t1 = 0* j by ;
then A27: (D . ('not' t1)) `2 = y by A24;
dd = t . ((len t1) + 1) by
.= ((j + 1) |-> 0) . (j + 1) by A26
.= FALSE ;
then 'not' dd = 1 ;
then A28: 'not' t = ('not' t1) ^ <*1*> by ;
reconsider nt1 = 'not' t1 as Node of D by ;
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 ^ ) = [a1,b] & D . (nt1 ^ <*1*>) = [b,b1] & dist (a1,b1) = 2 * (dist (a1,b)) & dist (a1,b1) = 2 * (dist (b,b1)) ) by ;
hence (D . ()) `2 = b1 by A28
.= y by ;
:: thesis: verum
end;
A31: S2[1]
proof
reconsider pusty = <*> {0,1} as Node of D by ;
let t be Tuple of 1, BOOLEAN ; :: thesis: ( t = 0* 1 implies (D . ()) `2 = y )
A32: ex b being Element of the carrier of V st
( D . (pusty ^ ) = [x,b] & D . (pusty ^ <*1*>) = [b,y] & dist (x,y) = 2 * (dist (x,b)) & dist (x,y) = 2 * (dist (b,y)) ) by ;
assume t = 0* 1 ; :: thesis: (D . ()) `2 = y
then t = by FINSEQ_2:59;
hence (D . ()) `2 = (D . (pusty ^ <*1*>)) `2 by
.= y by A32 ;
:: thesis: verum
end;
A33: for j being non zero Nat holds S2[j] from deffunc H2( 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 = H2(k) from A36: dom h = Seg N by ;
A37: 1 <= N by NAT_1:14;
then A38: 1 in Seg N by FINSEQ_1:1;
then A39: 1 in dom h by ;
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) + () by FINSEQ_1:22
.= (len h) + 1 by FINSEQ_1:39 ;
1 <= N + 1 by NAT_1:11;
hence f /. 1 = f . 1 by
.= h . 1 by
.= (g /. 1) `1 by
.= (g . 1) `1 by
.= (D . (FSL /. 1)) `1 by
.= (D . ((FinSeqLevel (n,dD)) . 1)) `1 by
.= (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 ;
then len f in dom f by FINSEQ_1:def 3;
hence A41: f /. (len f) = (h ^ <*y*>) . ((len h) + 1) by
.= 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
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 S4[ 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;
A46: now :: thesis: f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2
per cases ( i < (len f) - 1 or i = (len f) - 1 ) by ;
suppose i < (len f) - 1 ; :: thesis: f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2
then i < (len f) -' 1 by ;
then i + 1 <= (len f) -' 1 by NAT_1:13;
then A47: i + 1 <= (len f) - 1 by ;
then A48: (i + 1) - 1 <= (2 to_power n) - 1 by ;
defpred S5[ 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 S5[n] holds
S5[n + 1]
proof
let n be non zero Nat; :: thesis: ( S5[n] implies S5[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 ;
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: S5[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 ;
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 ;
then i < ((2 to_power (n + 1)) -' 1) + 1 by NAT_1:13;
then A56: i < ((2 to_power (n + 1)) - 1) + 1 by ;
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 ;
then ((i + 1) + 1) div 2 >= 1 by NAT_2:13;
then ((i + 1) + 1) div 2 in Seg (2 to_power n) by ;
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 ;
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 ;
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 ;
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 ;
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 ;
consider d being Element of the carrier of V such that
A63: D . (F1 ^ ) = [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 ;
consider d9 being Element of the carrier of V such that
A65: D . (FF1 ^ ) = [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 ;
A67: i = (i + 1) - 1
.= (i + 1) -' 1 by ;
now :: thesis: (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2
per cases ( i is odd or i is even ) ;
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 ;
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 ;
thus (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . (FF ^ <*(((2 * 1) + i) mod 2)*>)) `1 by
.= (D . (FF ^ <*1*>)) `1 by
.= d by
.= (D . ()) `2 by A63
.= (D . (F ^ <*((ii + 1) mod 2)*>)) `2 by
.= (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 by ; :: thesis: verum
end;
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
.= ((i -' 1) + (2 * 1)) mod 2 by NAT_D:21
.= (((i -' 1) + 1) + 1) mod 2
.= (i + 1) mod 2 by ;
A72: 1 + (1 + i) >= 1 by NAT_1:11;
(1 + 1) + (i -' 1) = (1 + 1) + (i - 1) by
.= ((1 + 1) + i) - 1 ;
then 1 = (((1 + 1) + i) -' 1) mod 2 by ;
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 ;
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 ;
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
.= (D . (FF ^ )) `1 by
.= a19 by A65
.= (D . (F ^ <*1*>)) `2 by
.= (D . ((FinSeqLevel ((n + 1),dD)) . ii)) `2 by ; :: thesis: verum
end;
end;
end;
hence (D . ((FinSeqLevel ((n + 1),dD)) . (i + 1))) `1 = (D . ((FinSeqLevel ((n + 1),dD)) . i)) `2 ; :: thesis: verum
end;
A77: S5[1]
proof
reconsider pusty = <*> {0,1} as Node of D by ;
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 ^ ) = [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 ;
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 ;
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 ^ )) `2 by A79
.= () `2 by FINSEQ_1:34
.= (D . ((FinSeqLevel (1,dD)) . i)) `2 by ;
:: thesis: verum
end;
A82: for n being non zero Nat holds S5[n] from A83: 1 <= 1 + i by NAT_1:11;
then A84: i + 1 in Seg (len h) by ;
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
.= (g /. (i + 1)) `1 by A34, A35, A36, A84
.= (g . (i + 1)) `1 by
.= (D . (FSL /. (i + 1))) `1 by A13, A14, A34, A84
.= (D . ((FinSeqLevel (n,dD)) . (i + 1))) `1 by
.= (D . ((FinSeqLevel (n,dD)) . i)) `2 by ;
:: thesis: verum
end;
suppose A85: i = (len f) - 1 ; :: thesis: f /. (i + 1) = (D . ((FinSeqLevel (n,dD)) . i)) `2
hence f /. (i + 1) = (D . ('not' ze)) `2 by
.= (D . ((FinSeqLevel (n,dD)) . i)) `2 by ;
:: thesis: verum
end;
end;
end;
A86: for l being non zero Nat st S4[l] holds
S4[l + 1]
proof
let l be non zero Nat; :: thesis: ( S4[l] implies S4[l + 1] )
reconsider dDll = dD -level l as non empty set by ;
reconsider ll = l as non zero Element of NAT by ORDINAL1:def 12;
reconsider dDll1 = dD -level (l + 1) as non empty set by ;
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: S4[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
proof
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 reconsider j1 = (j + 1) div 2 as non zero Element of NAT ;
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 ;
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 ;
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 ;
(FinSeqLevel ((l + 1),dD)) . j in dDll1 by ;
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 ;
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 ^ ) = [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 ;
A100: (FinSeqLevel ((ll + 1),dD)) . j = FSLlprim ^ <*((j + 1) mod 2)*> by ;
then FSLl = FSLlprim by ;
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 ;
now :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))
per cases ( d = 0 or d = 1 ) by ;
suppose d = 0 ; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))
then ( DF1 = x1 & DF2 = b ) by ;
then 2 * (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2 by ;
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;
suppose d = 1 ; :: thesis: dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1))
then ( DF1 = b & DF2 = y1 ) by ;
then 2 * (dist (DF1,DF2)) = (((dist (x,y)) / (2 to_power l)) / 2) * 2 by ;
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;
end;
end;
hence dist (DF1,DF2) = (dist (x,y)) / (2 to_power (l + 1)) ; :: thesis: verum
end;
A103: S4[1]
proof
reconsider pusty = <*> {0,1} as Node of D by ;
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 ;
then j in dom (FinSeqLevel (1,dD)) by BINTREE2:20;
then reconsider FSL1j = (FinSeqLevel (1,dD)) . j as Element of dom D by ;
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 ;
then A107: j in Seg 2 by ;
now :: thesis: dist (DF1,DF2) = (dist (x,y)) / 2
per cases ( j = 1 or j = 2 ) by ;
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 ^ ) = [x,b] & D . (pusty ^ <*1*>) = [b,y] & dist (x,y) = 2 * (dist (x,b)) & dist (x,y) = 2 * (dist (b,y)) ) by ;
A110: D . (pusty ^ ) = D . by FINSEQ_1:34
.= D . FSL1j by
.= [DF1,DF2] by ;
then DF1 = x by ;
hence dist (DF1,DF2) = (dist (x,y)) / 2 by ; :: thesis: verum
end;
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 ^ ) = [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 ;
A114: D . (pusty ^ <*1*>) = D . <*1*> by FINSEQ_1:34
.= D . FSL1j by
.= [DF1,DF2] by ;
then DF1 = b by ;
hence dist (DF1,DF2) = (dist (x,y)) / 2 by ; :: thesis: verum
end;
end;
end;
hence dist (DF1,DF2) = (dist (x,y)) / (2 to_power 1) by POWER:25; :: thesis: verum
end;
A115: for l being non zero Nat holds S4[l] from A116: i in Seg (len h) by ;
then i in dom h by FINSEQ_1:def 3;
then f /. i = h /. i by FINSEQ_4:68
.= h . i by
.= (g /. i) `1 by
.= (g . i) `1 by
.= (D . (FSL /. i)) `1 by
.= (D . ((FinSeqLevel (n,dD)) . i)) `1 by ;
hence dist ((f /. i),(f /. (i + 1))) = (dist (x,y)) / N by A34, A40, A43, A44, A46, A115; :: thesis: verum
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 ;
then dist (x,y) < N * p by ;
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
thus rng F c= {((dist (x,y)) / N)} :: according to XBOOLE_0:def 10 :: thesis: {((dist (x,y)) / N)} c= rng F
proof
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 ;
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
.= dist ((f /. c1),(f /. (c1 + 1))) by
.= (dist (x,y)) / N by ;
hence a in {((dist (x,y)) / N)} by TARSKI:def 1; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {((dist (x,y)) / N)} or a in 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
.= F . 1 by ;
1 in Seg (len F) by ;
then 1 in dom F by FINSEQ_1:def 3;
hence a in rng F by ; :: thesis: verum
end;
dom F = Seg (len F) by FINSEQ_1:def 3;
then F = (len F) |-> ((dist (x,y)) / N) by ;
hence Sum F = ((N + 1) - 1) * ((dist (x,y)) / N) by
.= dist (x,y) by XCMPLX_1:87 ;
:: thesis: verum
end;
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 ) )

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
proof
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 ;
then i = 1 by ;
hence dist ((f /. i),(f /. (i + 1))) < p by ; :: thesis: verum
end;
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
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 ;
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
.= dist (x,y) by ;
then F = <*dxy*> by ;
then Sum F = dxy by FINSOP_1:11;
hence dist (x,y) = Sum F ; :: thesis: verum
end;
end;