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) * (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:56
.= (W-bound C) + (((E-bound C) - (W-bound C)) / 2) by Lm6
.= ((W-bound C) + (E-bound C)) / 2 ;
:: thesis: verum