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