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-min (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-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
S-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:45;
then consider m being Nat such that
A1: m in dom (Cage (C,n)) and
A2: (Cage (C,n)) . m = S-min (L~ (Cage (C,n))) by FINSEQ_2:11;
A3: (Cage (C,n)) /. m = S-min (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-min (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-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1)
A7: j <= width (Gauge (C,n)) by A4, MATRIX_1:39;

A8: now

assume j > 1 ; :: thesis: contradiction
then (S-min (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;

1 <= j by A4, MATRIX_1:39;
hence S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by A3, A5, A8, XXREAL_0:1; :: thesis: verum