let i, j, m, n be Nat; :: thesis: for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds
((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) implies ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1 )
set a = N-bound D;
set s = S-bound D;
set w = W-bound D;
set e = E-bound D;
set G = Gauge (D,n);
set M = Gauge (D,m);
assume ( 1 <= i & i <= len (Gauge (D,n)) ) ; :: thesis: ( not 1 <= j or not j <= len (Gauge (D,m)) or ( not ( n > 0 & m > 0 ) & not ( n = 0 & m = 0 ) ) or ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1 )
then A1: [(Center (Gauge (D,n))),i] in Indices (Gauge (D,n)) by Lm4;
assume ( 1 <= j & j <= len (Gauge (D,m)) ) ; :: thesis: ( ( not ( n > 0 & m > 0 ) & not ( n = 0 & m = 0 ) ) or ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1 )
then A2: [(Center (Gauge (D,m))),j] in Indices (Gauge (D,m)) by Lm4;
assume A3: ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) ; :: thesis: ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1

per cases ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) by A3;

suppose that A4: n > 0 and
A5: m > 0 ; :: thesis: ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1

thus ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((Center (Gauge (D,n))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by A1, JORDAN8:def 1
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((Center (Gauge (D,n))) - 2)) by EUCLID:52
.= (W-bound D) + (((E-bound D) - (W-bound D)) / 2) by A4, Lm6
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ m)) * ((Center (Gauge (D,m))) - 2)) by A5, Lm6
.= |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ m)) * ((Center (Gauge (D,m))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ m)) * (j - 2)))]| `1 by EUCLID:52
.= ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1 by A2, JORDAN8:def 1 ; :: thesis: verum

end;

suppose A6: ( n = 0 & m = 0 ) ; :: thesis: ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1

thus ((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((Center (Gauge (D,n))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by A1, JORDAN8:def 1
.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ m)) * ((Center (Gauge (D,m))) - 2)) by A6, EUCLID:52
.= |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ m)) * ((Center (Gauge (D,m))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ m)) * (j - 2)))]| `1 by EUCLID:52
.= ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1 by A2, JORDAN8:def 1 ; :: thesis: verum

end;

end;