let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n, i being Nat st 1 <= i & i <= len (Gauge (C,n)) & n > 0 holds
((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 = ((S-bound C) + (N-bound C)) / 2
let n, i be Nat; ( 1 <= i & i <= len (Gauge (C,n)) & n > 0 implies ((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 = ((S-bound C) + (N-bound C)) / 2 )
assume A1:
( 1 <= i & i <= len (Gauge (C,n)) )
; ( not n > 0 or ((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 = ((S-bound C) + (N-bound C)) / 2 )
len (Gauge (C,1)) >= 4
by JORDAN8:10;
then A2:
len (Gauge (C,1)) >= 1
by XXREAL_0:2;
assume
n > 0
; ((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 = ((S-bound C) + (N-bound C)) / 2
hence ((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 =
((Gauge (C,1)) * (1,(Center (Gauge (C,1))))) `2
by A1, A2, JORDAN1A:37
.=
((S-bound C) + (N-bound C)) / 2
by A2, JORDAN1A:39
;
verum