let a, b, i, m be Nat; for D being non empty Subset of (TOP-REAL 2) st 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) holds
((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1
let D be non empty Subset of (TOP-REAL 2); ( 2 <= m & m < len (Gauge (D,i)) & 1 <= a & a <= len (Gauge (D,i)) & 1 <= b & b <= len (Gauge (D,(i + 1))) implies ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1 )
set I = Gauge (D,i);
set J = Gauge (D,(i + 1));
set z = N-bound D;
set e = E-bound D;
set s = S-bound D;
set w = W-bound D;
assume that
A1:
2 <= m
and
A2:
m < len (Gauge (D,i))
and
A3:
1 <= a
and
A4:
a <= len (Gauge (D,i))
and
A5:
1 <= b
and
A6:
b <= len (Gauge (D,(i + 1)))
; ((Gauge (D,i)) * (m,a)) `1 = ((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1
m < (2 |^ i) + 3
by A2, JORDAN8:def 1;
then
(2 * m) -' 2 <= (2 |^ (i + 1)) + 3
by Lm13;
then A7:
(2 * m) -' 2 <= len (Gauge (D,(i + 1)))
by JORDAN8:def 1;
A8:
len (Gauge (D,(i + 1))) = width (Gauge (D,(i + 1)))
by JORDAN8:def 1;
1 <= (2 * m) -' 2
by A1, Lm11;
then A9:
[((2 * m) -' 2),b] in Indices (Gauge (D,(i + 1)))
by A5, A6, A8, A7, MATRIX_0:30;
A10:
len (Gauge (D,i)) = width (Gauge (D,i))
by JORDAN8:def 1;
1 <= m
by A1, XXREAL_0:2;
then
[m,a] in Indices (Gauge (D,i))
by A2, A3, A4, A10, MATRIX_0:30;
hence ((Gauge (D,i)) * (m,a)) `1 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (m - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (a - 2)))]| `1
by JORDAN8:def 1
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (m - 2))
by EUCLID:52
.=
(W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2))
by A1, Lm10
.=
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (((2 * m) -' 2) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (b - 2)))]| `1
by EUCLID:52
.=
((Gauge (D,(i + 1))) * (((2 * m) -' 2),b)) `1
by A9, JORDAN8:def 1
;
verum