let p be polyhedron; :: thesis: for k being Integer holds len (k -polytope-seq p) = num-polytopes p,k
let k be Integer; :: thesis: len (k -polytope-seq p) = num-polytopes p,k
dom (k -polytope-seq p) = Seg (num-polytopes p,k) by Th28;
hence len (k -polytope-seq p) = num-polytopes p,k by FINSEQ_1:def 3; :: thesis: verum