let p be polyhedron; :: thesis: for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
let k be Integer; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
set F = the PolytopsF of p;

per cases ( k < - 1 or ( - 1 <= k & k <= dim p ) or k > dim p ) ;

suppose k < - 1 ; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

then ( k -polytope-seq p = <*> {} & k -polytopes p = {} ) by Def5, Def7;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by FINSEQ_1:def 3; :: thesis: verum

end;

suppose A1: ( - 1 <= k & k <= dim p ) ; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

per cases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A1, XXREAL_0:1;

suppose A2: k = - 1 ; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

then k -polytope-seq p = <*{}*> by Def7;
then A3: len (k -polytope-seq p) = 1 by FINSEQ_1:39;
k -polytopes p = {{}} by A2, Def5;
then num-polytopes (p,k) = 1 by CARD_2:42;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def 3; :: thesis: verum

end;

suppose A4: ( - 1 < k & k < dim p ) ; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

set n = k + 1;
reconsider n = k + 1 as Nat by A4, Th22;
reconsider Fn = the PolytopsF of p . n as FinSequence ;
( 1 <= n & n <= dim p ) by A4, Th22;
then A5: Fn is one-to-one by Def3;
k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A4, Def5;
then num-polytopes (p,k) = card (dom Fn) by A5, CARD_1:70;
then A6: len Fn = num-polytopes (p,k) by CARD_1:62;
k -polytope-seq p = the PolytopsF of p . (k + 1) by A4, Def7;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A6, FINSEQ_1:def 3; :: thesis: verum

end;

suppose A7: k = dim p ; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

then k -polytope-seq p = <*p*> by Def7;
then A8: len (k -polytope-seq p) = 1 by FINSEQ_1:39;
k -polytopes p = {p} by A7, Def5;
then num-polytopes (p,k) = 1 by CARD_2:42;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A8, FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

suppose k > dim p ; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

then ( k -polytope-seq p = <*> {} & k -polytopes p = {} ) by Def5, Def7;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by FINSEQ_1:def 3; :: thesis: verum

end;

end;