let p be polyhedron; :: thesis: 1 -th-polytope p,(dim p) = p
reconsider egy = 1 as Nat ;
A1: egy <= num-polytopes p,(dim p) by Th32;
set s = (dim p) -polytope-seq p;
A2: (dim p) -polytope-seq p = <*p*> by Def7;
egy -th-polytope p,(dim p) = ((dim p) -polytope-seq p) . egy by A1, Def12
.= p by A2, FINSEQ_1:57 ;
hence 1 -th-polytope p,(dim p) = p ; :: thesis: verum