let j, n be Nat; :: thesis: for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge (T,n)) holds
((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T
let T be non empty Subset of (TOP-REAL 2); :: thesis: ( 1 <= j & j <= len (Gauge (T,n)) implies ((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T )
set G = Gauge (T,n);
set W = W-bound T;
set S = S-bound T;
set E = E-bound T;
set N = N-bound T;
assume that
A1: 1 <= j and
A2: j <= len (Gauge (T,n)) ; :: thesis: ((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = E-bound T
A3: len (Gauge (T,n)) = (2 |^ n) + 3 by Def1;
A4: len (Gauge (T,n)) = width (Gauge (T,n)) by Def1;
A5: len (Gauge (T,n)) >= 4 by Th10;
then 1 < len (Gauge (T,n)) by XXREAL_0:2;
then A6: 1 <= (len (Gauge (T,n))) -' 1 by NAT_D:49;
A7: ((len (Gauge (T,n))) -' 1) - 2 = ((len (Gauge (T,n))) - 1) - 2 by A5, XREAL_1:233, XXREAL_0:2
.= 2 |^ n by A3 ;
A8: 2 |^ n > 0 by NEWTON:83;
(len (Gauge (T,n))) -' 1 <= len (Gauge (T,n)) by NAT_D:35;
then [((len (Gauge (T,n))) -' 1),j] in Indices (Gauge (T,n)) by A1, A2, A4, A6, MATRIX_0:30;
then (Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j) = |[((W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (((len (Gauge (T,n))) -' 1) - 2))),((S-bound T) + ((((N-bound T) - (S-bound T)) / (2 |^ n)) * (j - 2)))]| by Def1;
hence ((Gauge (T,n)) * (((len (Gauge (T,n))) -' 1),j)) `1 = (W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (2 |^ n)) by A7, EUCLID:52
.= (W-bound T) + ((E-bound T) - (W-bound T)) by A8, XCMPLX_1:87
.= E-bound T ;
:: thesis: verum