let i, j, n be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st [i,j] in Indices (Gauge C,n) & [(i + 1),j] in Indices (Gauge C,n) holds
dist ((Gauge C,n) * i,j),((Gauge C,n) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( [i,j] in Indices (Gauge C,n) & [(i + 1),j] in Indices (Gauge C,n) implies dist ((Gauge C,n) * i,j),((Gauge C,n) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ n) )
set G = Gauge C,n;
set a = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
set p1 = (Gauge C,n) * i,j;
set p2 = (Gauge C,n) * (i + 1),j;
assume that
A1: [i,j] in Indices (Gauge C,n) and
A2: [(i + 1),j] in Indices (Gauge C,n) ; :: thesis: dist ((Gauge C,n) * i,j),((Gauge C,n) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ n)
consider p, q being Point of (Euclid 2) such that
A3: ( p = (Gauge C,n) * i,j & q = (Gauge C,n) * (i + 1),j ) and
A4: dist ((Gauge C,n) * i,j),((Gauge C,n) * (i + 1),j) = dist p,q by TOPREAL6:def 1;
A5: (Gauge C,n) * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A1, JORDAN8:def 1;
A6: (Gauge C,n) * (i + 1),j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| by A2, JORDAN8:def 1;
set x = ((E-bound C) - (W-bound C)) / (2 |^ n);
E-bound C >= W-bound C by SPRECT_1:23;
then A7: (E-bound C) - (W-bound C) >= (W-bound C) - (W-bound C) by XREAL_1:11;
dist p,q = (Pitag_dist 2) . p,q by METRIC_1:def 1
.= sqrt ((((((Gauge C,n) * i,j) `1 ) - (((Gauge C,n) * (i + 1),j) `1 )) ^2 ) + (((((Gauge C,n) * i,j) `2 ) - (((Gauge C,n) * (i + 1),j) `2 )) ^2 )) by A3, TOPREAL3:12
.= sqrt ((((((Gauge C,n) * i,j) `1 ) - (((Gauge C,n) * (i + 1),j) `1 )) ^2 ) + ((((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - (((Gauge C,n) * (i + 1),j) `2 )) ^2 )) by A5, EUCLID:56
.= sqrt ((((((Gauge C,n) * i,j) `1 ) - (((Gauge C,n) * (i + 1),j) `1 )) ^2 ) + ((((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - ((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))) ^2 )) by A6, EUCLID:56
.= abs ((((Gauge C,n) * i,j) `1 ) - (((Gauge C,n) * (i + 1),j) `1 )) by COMPLEX1:158
.= abs (((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - (((Gauge C,n) * (i + 1),j) `1 )) by A5, EUCLID:56
.= abs (((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - ((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((i + 1) - 2)))) by A6, EUCLID:56
.= abs (- (((E-bound C) - (W-bound C)) / (2 |^ n)))
.= abs (((E-bound C) - (W-bound C)) / (2 |^ n)) by COMPLEX1:138
.= (abs ((E-bound C) - (W-bound C))) / (abs (2 |^ n)) by COMPLEX1:153
.= ((E-bound C) - (W-bound C)) / (abs (2 |^ n)) by A7, ABSVALUE:def 1 ;
hence dist ((Gauge C,n) * i,j),((Gauge C,n) * (i + 1),j) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A4, ABSVALUE:def 1; :: thesis: verum