let n be Nat; 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-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1) )
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ex i being 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:42;
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:10;
A3:
(Cage (C,n)) /. m = S-max (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
; ( 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_0:32; S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1)
A7:
j <= width (Gauge (C,n))
by A4, MATRIX_0:32;
A8:
now not j > 1assume
j > 1
;
contradictionthen
(S-max (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;
verum end;
1 <= j
by A4, MATRIX_0:32;
hence
S-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (i,1)
by A3, A5, A8, XXREAL_0:1; verum