let i, j, m, n be Nat; :: thesis:
let D be non empty Subset of (TOP-REAL 2); :: thesis:
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:
then A1: [i,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) by Lm5;
assume ( 1 <= j & j <= len (Gauge (D,m)) ) ; :: thesis:
then A2: [j,(Center (Gauge (D,m)))] in Indices (Gauge (D,m)) by Lm5;
assume A3: ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) ; :: thesis:

per cases by A3;

suppose that A4: n > 0 and
A5: m > 0 ; :: thesis:

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

end;

suppose A6: ( n = 0 & m = 0 ) ; :: thesis:

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

end;

end;