let i, n be Nat; 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); ( 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))
; ((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 Th10;
then
2 <= len (Gauge (T,n))
by XXREAL_0:2;
then
[i,2] in Indices (Gauge (T,n))
by A1, A2, A3, MATRIX_0:30;
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:52; verum