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 A1: k < - 1 ; :: thesis: dom (k -polytope-seq p) = Seg (num-polytopes p,k)

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

end;

suppose A3: ( - 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 A3, XXREAL_0:1;

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

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

end;

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

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

end;

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

then A12: k -polytopes p = {p} by Def5;
A13: k -polytope-seq p = <*p*> by A11, Def7;
A14: num-polytopes p,k = 1 by A12, CARD_2:60;
len (k -polytope-seq p) = 1 by A13, FINSEQ_1:56;
hence dom (k -polytope-seq p) = Seg (num-polytopes p,k) by A14, FINSEQ_1:def 3; :: thesis: verum

end;

end;

end;

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

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

end;

end;