let i, n, j, m be Element of 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:56
.= (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:56
.= ((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:56
.= |[((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:56
.= ((Gauge D,m) * (Center (Gauge D,m)),j) `1 by A2, JORDAN8:def 1 ; :: thesis: verum

end;

end;