let i, j, m, n be Nat; :: thesis: for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds
((Gauge (E,m)) * (1,j)) `1 <= ((Gauge (E,n)) * (1,i)) `1
let E be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n implies ((Gauge (E,m)) * (1,j)) `1 <= ((Gauge (E,n)) * (1,i)) `1 )
set w = W-bound E;
set e = E-bound E;
set G = Gauge (E,n);
set M = Gauge (E,m);
assume that
A1: ( 1 <= i & i <= len (Gauge (E,n)) ) and
A2: ( 1 <= j & j <= len (Gauge (E,m)) ) and
A3: m <= n ; :: thesis: ((Gauge (E,m)) * (1,j)) `1 <= ((Gauge (E,n)) * (1,i)) `1
A4: len (Gauge (E,m)) = width (Gauge (E,m)) by JORDAN8:def 1;
1 <= len (Gauge (E,m)) by A2, XXREAL_0:2;
then [1,j] in Indices (Gauge (E,m)) by A2, A4, MATRIX_0:30;
then A5: ((Gauge (E,m)) * (1,j)) `1 = (W-bound E) - (((E-bound E) - (W-bound E)) / (2 |^ m)) by Lm12;
A6: len (Gauge (E,n)) = width (Gauge (E,n)) by JORDAN8:def 1;
1 <= len (Gauge (E,n)) by A1, XXREAL_0:2;
then [1,i] in Indices (Gauge (E,n)) by A1, A6, MATRIX_0:30;
then ( 0 < (E-bound E) - (W-bound E) & ((Gauge (E,n)) * (1,i)) `1 = (W-bound E) - (((E-bound E) - (W-bound E)) / (2 |^ n)) ) by Lm12, SPRECT_1:31, XREAL_1:50;
hence ((Gauge (E,m)) * (1,j)) `1 <= ((Gauge (E,n)) * (1,i)) `1 by A3, A5, Lm9; :: thesis: verum