let i, j, n be 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)
A3: (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;
N-bound C >= S-bound C by SPRECT_1:22;
then A4: (N-bound C) - (S-bound C) >= (S-bound C) - (S-bound C) by XREAL_1:9;
set x = ((N-bound C) - (S-bound C)) / (2 |^ n);
consider p, q being Point of (Euclid 2) such that
A5: ( p = (Gauge (C,n)) * (i,j) & q = (Gauge (C,n)) * (i,(j + 1)) ) and
A6: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = dist (p,q) by TOPREAL6:def 1;
A7: (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;
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 A5, TOPREAL3:7
.= 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 A7, EUCLID:52
.= 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 A3, EUCLID:52
.= |.((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * (i,(j + 1))) `2)).| by COMPLEX1:72
.= |.(((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2))) - (((Gauge (C,n)) * (i,(j + 1))) `2)).| by A7, EUCLID:52
.= |.(((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 A3, EUCLID:52
.= |.(- (((N-bound C) - (S-bound C)) / (2 |^ n))).|
.= |.(((N-bound C) - (S-bound C)) / (2 |^ n)).| by COMPLEX1:52
.= |.((N-bound C) - (S-bound C)).| / |.(2 |^ n).| by COMPLEX1:67
.= ((N-bound C) - (S-bound C)) / |.(2 |^ n).| by A4, 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 A6, ABSVALUE:def 1; :: thesis: verum