let i, n be Element of NAT ; :: thesis: for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge T,n) holds
((Gauge T,n) * i,2) `2 = S-bound T
let T be non empty Subset of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= len (Gauge T,n) implies ((Gauge T,n) * i,2) `2 = S-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 <= i and
A2: i <= len (Gauge T,n) ; :: thesis: ((Gauge T,n) * i,2) `2 = S-bound T
A3: len (Gauge T,n) = width (Gauge T,n) by Def1;
len (Gauge T,n) >= 4 by Th13;
then 2 <= len (Gauge T,n) by XXREAL_0:2;
then [i,2] in Indices (Gauge T,n) by A1, A2, A3, MATRIX_1:37;
then (Gauge T,n) * i,2 = |[((W-bound T) + ((((E-bound T) - (W-bound T)) / (2 |^ n)) * (i - 2))),((S-bound T) + ((((N-bound T) - (S-bound T)) / (2 |^ n)) * (2 - 2)))]| by Def1;
hence ((Gauge T,n) * i,2) `2 = S-bound T by EUCLID:56; :: thesis: verum