let i, j, m, n be Nat; :: thesis: for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge (D,m)) & 1 < j & j < width (Gauge (D,m)) holds
for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
(Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1)
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( m <= n & 1 < i & i < len (Gauge (D,m)) & 1 < j & j < width (Gauge (D,m)) implies for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
(Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1) )
assume that
A1: m <= n and
A2: ( 1 < i & i < len (Gauge (D,m)) ) and
A3: ( 1 < j & j < width (Gauge (D,m)) ) ; :: thesis: for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds
(Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1)
let i1, j1 be Nat; :: thesis: ( i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 implies (Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1) )
assume that
A4: i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 and
A5: j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 ; :: thesis: (Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1)
A6: ( 1 < i1 & i1 < len (Gauge (D,n)) ) by A1, A2, A4, Th31;
(j - 2) / (2 |^ m) = (j - 2) / (2 |^ (n -' (n -' m))) by A1, NAT_D:58
.= (j - 2) / ((2 |^ n) / (2 |^ (n -' m))) by NAT_D:50, TOPREAL6:10
.= (j1 - 2) / (2 |^ n) by A5, XCMPLX_1:77 ;
then A7: (((N-bound D) - (S-bound D)) / (2 |^ m)) * (j - 2) = ((N-bound D) - (S-bound D)) * ((j1 - 2) / (2 |^ n)) by XCMPLX_1:75
.= (((N-bound D) - (S-bound D)) / (2 |^ n)) * (j1 - 2) by XCMPLX_1:75 ;
(i - 2) / (2 |^ m) = (i - 2) / (2 |^ (n -' (n -' m))) by A1, NAT_D:58
.= (i - 2) / ((2 |^ n) / (2 |^ (n -' m))) by NAT_D:50, TOPREAL6:10
.= (i1 - 2) / (2 |^ n) by A4, XCMPLX_1:77 ;
then A8: (((E-bound D) - (W-bound D)) / (2 |^ m)) * (i - 2) = ((E-bound D) - (W-bound D)) * ((i1 - 2) / (2 |^ n)) by XCMPLX_1:75
.= (((E-bound D) - (W-bound D)) / (2 |^ n)) * (i1 - 2) by XCMPLX_1:75 ;
( 1 < j1 & j1 < width (Gauge (D,n)) ) by A1, A3, A5, Th32;
then A9: [i1,j1] in Indices (Gauge (D,n)) by A6, MATRIX_0:30;
[i,j] in Indices (Gauge (D,m)) by A2, A3, MATRIX_0:30;
hence (Gauge (D,m)) * (i,j) = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ m)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ m)) * (j - 2)))]| by JORDAN8:def 1
.= (Gauge (D,n)) * (i1,j1) by A9, A8, A7, JORDAN8:def 1 ;
:: thesis: verum