let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n, i being Nat st 1 <= i & i <= width (Gauge (C,n)) & n > 0 holds

((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2

let n, i be Nat; :: thesis: ( 1 <= i & i <= width (Gauge (C,n)) & n > 0 implies ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 )

assume A1: ( 1 <= i & i <= width (Gauge (C,n)) ) ; :: thesis: ( not n > 0 or ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 )

reconsider ii = i as Nat ;

A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

assume A3: n > 0 ; :: thesis: ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2

len (Gauge (C,1)) >= 4 by JORDAN8:10;

then A4: len (Gauge (C,1)) >= 1 by XXREAL_0:2;

thus ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),ii)) `1

.= ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A1, A2, A4, A3, JORDAN1A:36

.= ((W-bound C) + (E-bound C)) / 2 by A4, JORDAN1A:38 ; :: thesis: verum

((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2

let n, i be Nat; :: thesis: ( 1 <= i & i <= width (Gauge (C,n)) & n > 0 implies ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 )

assume A1: ( 1 <= i & i <= width (Gauge (C,n)) ) ; :: thesis: ( not n > 0 or ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2 )

reconsider ii = i as Nat ;

A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;

assume A3: n > 0 ; :: thesis: ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((W-bound C) + (E-bound C)) / 2

len (Gauge (C,1)) >= 4 by JORDAN8:10;

then A4: len (Gauge (C,1)) >= 1 by XXREAL_0:2;

thus ((Gauge (C,n)) * ((Center (Gauge (C,n))),i)) `1 = ((Gauge (C,n)) * ((Center (Gauge (C,n))),ii)) `1

.= ((Gauge (C,1)) * ((Center (Gauge (C,1))),1)) `1 by A1, A2, A4, A3, JORDAN1A:36

.= ((W-bound C) + (E-bound C)) / 2 by A4, JORDAN1A:38 ; :: thesis: verum