let i be Element of 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:56
.= (S-bound C) + (((N-bound C) - (S-bound C)) / 2) by Lm6
.= ((S-bound C) + (N-bound C)) / 2 ;
:: thesis: verum