let i be Nat; 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); ( 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)) )
; ((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
;
verum