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,(j + 1)] in Indices (Gauge C,n) holds
dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) = ((N-bound C) - (S-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,(j + 1)] in Indices (Gauge C,n) implies dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) = ((N-bound C) - (S-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,(j + 1);
assume that
A1: [i,j] in Indices (Gauge C,n) and
A2: [i,(j + 1)] in Indices (Gauge C,n) ; :: thesis: dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) = ((N-bound C) - (S-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,(j + 1) ) and
A4: dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) = 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,(j + 1) = |[((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 + 1) - 2)))]| by A2, JORDAN8:def 1;
set x = ((N-bound C) - (S-bound C)) / (2 |^ n);
N-bound C >= S-bound C by SPRECT_1:24;
then A7: (N-bound C) - (S-bound C) >= (S-bound C) - (S-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,(j + 1)) `1 )) ^2 ) + (((((Gauge C,n) * i,j) `2 ) - (((Gauge C,n) * i,(j + 1)) `2 )) ^2 )) by A3, TOPREAL3:12
.= sqrt (((((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - (((Gauge C,n) * i,(j + 1)) `1 )) ^2 ) + (((((Gauge C,n) * i,j) `2 ) - (((Gauge C,n) * i,(j + 1)) `2 )) ^2 )) by A5, EUCLID:56
.= sqrt (((((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 - 2)))) ^2 ) + (((((Gauge C,n) * i,j) `2 ) - (((Gauge C,n) * i,(j + 1)) `2 )) ^2 )) by A6, EUCLID:56
.= abs ((((Gauge C,n) * i,j) `2 ) - (((Gauge C,n) * i,(j + 1)) `2 )) by COMPLEX1:158
.= abs (((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - (((Gauge C,n) * i,(j + 1)) `2 )) by A5, EUCLID:56
.= abs (((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 + 1) - 2)))) by A6, EUCLID:56
.= abs (- (((N-bound C) - (S-bound C)) / (2 |^ n)))
.= abs (((N-bound C) - (S-bound C)) / (2 |^ n)) by COMPLEX1:138
.= (abs ((N-bound C) - (S-bound C))) / (abs (2 |^ n)) by COMPLEX1:153
.= ((N-bound C) - (S-bound C)) / (abs (2 |^ n)) by A7, ABSVALUE:def 1 ;
hence dist ((Gauge C,n) * i,j),((Gauge C,n) * i,(j + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A4, ABSVALUE:def 1; :: thesis: verum