let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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; :: thesis: ( 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)) ) ; :: thesis: ( 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 ; :: thesis: ((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 ;

:: thesis: verum

((Gauge (C,n)) * (i,(Center (Gauge (C,n))))) `2 = ((S-bound C) + (N-bound C)) / 2

let n, i be Nat; :: thesis: ( 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)) ) ; :: thesis: ( 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 ; :: thesis: ((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 ;

:: thesis: verum