let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ex i being Nat st
( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
A1: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
N-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:40;
then consider m being Nat such that
A2: m in dom (Cage (C,n)) and
A3: (Cage (C,n)) . m = N-max (L~ (Cage (C,n))) by FINSEQ_2:10;
A4: (Cage (C,n)) /. m = N-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 i ; :: thesis: ( 1 <= i & i <= len (Gauge (C,n)) & N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) )
thus A7: ( 1 <= i & i <= len (Gauge (C,n)) ) by A5, MATRIX_0:32; :: thesis: N-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,(width (Gauge (C,n))))
A8: 1 <= j by A5, MATRIX_0:32;

A9: now :: thesis: not j < width (Gauge (C,n))

assume j < width (Gauge (C,n)) ; :: thesis: contradiction
then (N-max (L~ (Cage (C,n)))) `2 < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by A4, A6, A7, A8, GOBOARD5:4;
then N-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 by EUCLID:52;
hence contradiction by A7, A1, JORDAN1A:70; :: thesis: verum

end;

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