let C be connected compact non horizontal non vertical Subset of ; :: thesis: for n being Element of NAT
for 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 be Element of NAT ; :: thesis: for 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 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 Element of NAT by ORDINAL1:def 13;
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:13;
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:57
.= ((W-bound C) + (E-bound C)) / 2 by A4, JORDAN1A:59 ; :: thesis: verum