let n, i, a, b be Element of NAT ; :: thesis:
let D be non empty Subset of (TOP-REAL 2); :: thesis:
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 <= n and
A2: n < len (Gauge D,i) and
A3: ( 1 <= a & a <= len (Gauge D,i) ) and
A4: ( 1 <= b & b <= len (Gauge D,(i + 1)) ) ; :: thesis:
A5: len (Gauge D,i) = width (Gauge D,i) by JORDAN8:def 1;
A6: len (Gauge D,(i + 1)) = width (Gauge D,(i + 1)) by JORDAN8:def 1;
A7: 1 <= (2 * n) -' 2 by A1, Lm11;
n < (2 |^ i) + 3 by A2, JORDAN8:def 1;
then (2 * n) -' 2 <= (2 |^ (i + 1)) + 3 by Lm13;
then (2 * n) -' 2 <= len (Gauge D,(i + 1)) by JORDAN8:def 1;
then A8: [b,((2 * n) -' 2)] in Indices (Gauge D,(i + 1)) by A4, A6, A7, MATRIX_1:37;
1 <= n by A1, XXREAL_0:2;
then [a,n] in Indices (Gauge D,i) by A2, A3, A5, MATRIX_1:37;
hence ((Gauge D,i) * a,n) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ i)) * (a - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (n - 2)))]| `2 by JORDAN8:def 1
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ i)) * (n - 2)) by EUCLID:56
.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2)) by A1, Lm10
.= |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ (i + 1))) * (b - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ (i + 1))) * (((2 * n) -' 2) - 2)))]| `2 by EUCLID:56
.= ((Gauge D,(i + 1)) * b,((2 * n) -' 2)) `2 by A8, JORDAN8:def 1 ;
:: thesis: