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)) & 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 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:41;
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:10;
A3: (Cage (C,n)) /. m = S-min (L~ (Cage (C,n))) by A1, A2, PARTFUN1:def 6;
Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def 1;
then consider i, j being 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 9;
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_0:32; :: thesis: S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1)
A7: j <= width (Gauge (C,n)) by A4, MATRIX_0:32;
A8: now :: thesis: not j > 1
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:4;
then S-bound (L~ (Cage (C,n))) > ((Gauge (C,n)) * (i,1)) `2 by EUCLID:52;
hence contradiction by A6, JORDAN1A:72; :: thesis: verum
end;
1 <= j by A4, MATRIX_0:32;
hence S-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) by A3, A5, A8, XXREAL_0:1; :: thesis: verum