let i be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds
((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = ((W-bound C) + (E-bound C)) / 2
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( 1 <= i & i <= len (Gauge (C,1)) implies ((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 )
set a = N-bound C;
set s = S-bound C;
set w = W-bound C;
set e = E-bound C;
set G = Gauge (C,1);
assume ( 1 <= i & i <= len (Gauge (C,1)) ) ; :: thesis: ((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = ((W-bound C) + (E-bound C)) / 2
then [(Center (Gauge (C,1))),i] in Indices (Gauge (C,1)) by Lm4;
hence ((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ 1)) * ((Center (Gauge (C,1))) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ 1)) * (i - 2)))]| `1 by JORDAN8:def 1
.= (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ 1)) * ((Center (Gauge (C,1))) - 2)) by EUCLID:52
.= (W-bound C) + (((E-bound C) - (W-bound C)) / 2) by Lm6
.= ((W-bound C) + (E-bound C)) / 2 ;
:: thesis: verum