n in Seg (num-polytopes p,k) by A1, FINSEQ_1:3;
then n in dom (k -polytope-seq p) by Th28;
then (k -polytope-seq p) . n in rng (k -polytope-seq p) by FUNCT_1:12;
hence (k -polytope-seq p) . n is Element of k -polytopes p by Th30; :: thesis: verum