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 + 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)
A3: (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;
E-bound C >= W-bound C by SPRECT_1:21;
then A4: (E-bound C) - (W-bound C) >= (W-bound C) - (W-bound C) by XREAL_1:9;
set x = ((E-bound C) - (W-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 + 1),j) ) and
A6: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = 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 + 1),j)) `1)) ^2) + (((((Gauge (C,n)) * (i,j)) `2) - (((Gauge (C,n)) * ((i + 1),j)) `2)) ^2)) by A5, TOPREAL3:7
.= 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 A7
.= 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 A3
.= |.((((Gauge (C,n)) * (i,j)) `1) - (((Gauge (C,n)) * ((i + 1),j)) `1)).| by COMPLEX1:72
.= |.(((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))) - (((Gauge (C,n)) * ((i + 1),j)) `1)).| by A7
.= |.(((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 A3
.= |.(- (((E-bound C) - (W-bound C)) / (2 |^ n))).|
.= |.(((E-bound C) - (W-bound C)) / (2 |^ n)).| by COMPLEX1:52
.= |.((E-bound C) - (W-bound C)).| / |.(2 |^ n).| by COMPLEX1:67
.= ((E-bound C) - (W-bound C)) / |.(2 |^ n).| by A4, 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 A6, ABSVALUE:def 1; :: thesis: verum