let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & S-max (L~ (Cage C,n)) = (Gauge C,n) * i,1 )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex i being Element of NAT st
( 1 <= i & i <= len (Gauge C,n) & S-max (L~ (Cage C,n)) = (Gauge C,n) * i,1 )
S-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:46;
then consider m being Nat such that
A1: m in dom (Cage C,n) and
A2: (Cage C,n) . m = S-max (L~ (Cage C,n)) by FINSEQ_2:11;
A3: (Cage C,n) /. m = S-max (L~ (Cage C,n)) by A1, A2, PARTFUN1:def 8;
Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then consider i, j being Element of NAT such that
A4: [i,j] in Indices (Gauge C,n) and
A5: (Cage C,n) /. m = (Gauge C,n) * i,j by A1, GOBOARD1:def 11;
take i ; :: thesis: ( 1 <= i & i <= len (Gauge C,n) & S-max (L~ (Cage C,n)) = (Gauge C,n) * i,1 )
thus A6: ( 1 <= i & i <= len (Gauge C,n) ) by A4, MATRIX_1:39; :: thesis: S-max (L~ (Cage C,n)) = (Gauge C,n) * i,1
A7: ( 1 <= j & j <= width (Gauge C,n) ) by A4, MATRIX_1:39;

now

assume j > 1 ; :: thesis: contradiction
then (S-max (L~ (Cage C,n))) `2 > ((Gauge C,n) * i,1) `2 by A3, A5, A6, A7, GOBOARD5:5;
then S-bound (L~ (Cage C,n)) > ((Gauge C,n) * i,1) `2 by EUCLID:56;
hence contradiction by A6, JORDAN1A:93; :: thesis: verum

end;

hence S-max (L~ (Cage C,n)) = (Gauge C,n) * i,1 by A3, A5, A7, XXREAL_0:1; :: thesis: verum