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)) * (i,(Center (Gauge (C,1))))) `2 = ((S-bound C) + (N-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)) * (i,(Center (Gauge (C,1))))) `2 = ((S-bound C) + (N-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)) * (i,(Center (Gauge (C,1))))) `2 = ((S-bound C) + (N-bound C)) / 2
then [i,(Center (Gauge (C,1)))] in Indices (Gauge (C,1)) by Lm5;
hence ((Gauge (C,1)) * (i,(Center (Gauge (C,1))))) `2 = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ 1)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ 1)) * ((Center (Gauge (C,1))) - 2)))]| `2 by JORDAN8:def 1
.= (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ 1)) * ((Center (Gauge (C,1))) - 2)) by EUCLID:52
.= (S-bound C) + (((N-bound C) - (S-bound C)) / 2) by Lm6
.= ((S-bound C) + (N-bound C)) / 2 ;
:: thesis: verum