let C be Simple_closed_curve; :: thesis: for n being Element of NAT st 0 < n holds
ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )
let n be Element of NAT ; :: thesis: ( 0 < n implies ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i ) )
set f = Cage C,n;
set G = Gauge C,n;
set w = Center (Gauge C,n);
A1: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
A2: len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets Upper_Arc (L~ (Cage C,n)) by JORDAN1B:34;
then A3: LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n))) meets L~ (Cage C,n) by JORDAN6:76, XBOOLE_1:63;
A4: Center (Gauge C,n) <= len (Gauge C,n) by JORDAN1B:14;
assume A5: 0 < n ; :: thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )
then UMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(upper_bound (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by Th13;
then A6: (UMP (L~ (Cage C,n))) `2 = upper_bound (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) by EUCLID:56;
A7: 1 <= len (Gauge C,n) by Lm3;
A8: 1 <= Center (Gauge C,n) by JORDAN1B:12;
then A9: [(Center (Gauge C,n)),(len (Gauge C,n))] in Indices (Gauge C,n) by A2, A7, A4, MATRIX_1:37;
[(Center (Gauge C,n)),1] in Indices (Gauge C,n) by A2, A7, A8, A4, MATRIX_1:37;
then consider i being Element of NAT such that
A10: 1 <= i and
A11: i <= len (Gauge C,n) and
A12: ((Gauge C,n) * (Center (Gauge C,n)),i) `2 = upper_bound (proj2 .: ((LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))) /\ (L~ (Cage C,n)))) by A1, A3, A7, A9, JORDAN1F:2;
A13: (UMP (L~ (Cage C,n))) `1 = ((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2 by EUCLID:56;
take i ; :: thesis: ( 1 <= i & i <= len (Gauge C,n) & UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )
thus ( 1 <= i & i <= len (Gauge C,n) ) by A10, A11; :: thesis: UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i
((Gauge C,n) * (Center (Gauge C,n)),i) `1 = ((W-bound C) + (E-bound C)) / 2 by A5, A2, A10, A11, JORDAN1G:43;
then (UMP (L~ (Cage C,n))) `1 = ((Gauge C,n) * (Center (Gauge C,n)),i) `1 by A13, JORDAN1G:41;
hence UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i by A12, A6, TOPREAL3:11; :: thesis: verum