let n be Nat; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n))

let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n))

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A1: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by JORDAN1E:def 1;

then E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A1, FINSEQ_5:46;

then A2: Upper_Seq (C,n) just_once_values E-max (L~ (Cage (C,n))) by FINSEQ_4:8;

(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) by JORDAN1F:7;

hence (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n)) by A2, FINSEQ_6:166; :: thesis: verum

let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n))

E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;

then A1: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;

( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by JORDAN1E:def 1;

then E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A1, FINSEQ_5:46;

then A2: Upper_Seq (C,n) just_once_values E-max (L~ (Cage (C,n))) by FINSEQ_4:8;

(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n))) by JORDAN1F:7;

hence (E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n)) by A2, FINSEQ_6:166; :: thesis: verum