let i, j, m, n be Nat; 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); ( 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)) )
; ( 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)) )
; ( ( 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 ) )
; ((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
;
((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
;
verum end; suppose A6:
(
n = 0 &
m = 0 )
;
((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
;
verum end; end;