let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n, i being Element of 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 Element of 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:13;
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:58
.= ((S-bound C) + (N-bound C)) / 2 by A2, JORDAN1A:60 ;
:: thesis: verum