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 Th25;
hence len (k -polytope-seq p) = num-polytopes (p,k) by FINSEQ_1:def 3; :: thesis: verum