let m, n, i, j be Element of 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 Element of 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 Element of 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 Element of 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 Element of 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, Th52;
(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:15
.= (j1 - 2) / (2 |^ n) by A5, XCMPLX_1:78 ;
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:76
.= (((N-bound D) - (S-bound D)) / (2 |^ n)) * (j1 - 2) by XCMPLX_1:76 ;
(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:15
.= (i1 - 2) / (2 |^ n) by A4, XCMPLX_1:78 ;
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:76
.= (((E-bound D) - (W-bound D)) / (2 |^ n)) * (i1 - 2) by XCMPLX_1:76 ;
( 1 < j1 & j1 < width (Gauge D,n) ) by A1, A3, A5, Th53;
then A9: [i1,j1] in Indices (Gauge D,n) by A6, MATRIX_1:37;
[i,j] in Indices (Gauge D,m) by A2, A3, MATRIX_1:37;
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