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

A9: now :: thesis: not i < len (Gauge (C,n))

assume i < len (Gauge (C,n)) ; :: thesis: contradiction
then (E-max (L~ (Cage (C,n)))) `1 < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by A4, A6, A7, A8, GOBOARD5:3;
then E-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * ((len (Gauge (C,n))),j)) `1 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:71; :: thesis: verum

end;

i <= len (Gauge (C,n)) by A5, MATRIX_0:32;
hence E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * ((len (Gauge (C,n))),j) by A4, A6, A9, XXREAL_0:1; :: thesis: verum