let p be polyhedron; :: thesis: for k being Integer holds k -polytope-seq p is one-to-one
let k be Integer; :: thesis: k -polytope-seq p is one-to-one
set s = k -polytope-seq p;

per cases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;

suppose k < - 1 ; :: thesis: k -polytope-seq p is one-to-one

hence k -polytope-seq p is one-to-one by Def7; :: thesis: verum

end;

suppose k = - 1 ; :: thesis: k -polytope-seq p is one-to-one

hence k -polytope-seq p is one-to-one by Def7; :: thesis: verum

end;

suppose A1: ( - 1 < k & k < dim p ) ; :: thesis: k -polytope-seq p is one-to-one

then A2: (- 1) + 1 < k + 1 by XREAL_1:6;
then reconsider m = k + 1 as Element of NAT by INT_1:3;
set F = the PolytopsF of p;
A3: 0 + 1 <= m by A2, INT_1:7;
( k -polytope-seq p = the PolytopsF of p . (k + 1) & m <= dim p ) by A1, Def7, INT_1:7;
hence k -polytope-seq p is one-to-one by A3, Def3; :: thesis: verum

end;

suppose k = dim p ; :: thesis: k -polytope-seq p is one-to-one

then k -polytope-seq p = <*p*> by Def7;
hence k -polytope-seq p is one-to-one ; :: thesis: verum

end;

suppose k > dim p ; :: thesis: k -polytope-seq p is one-to-one

hence k -polytope-seq p is one-to-one by Def7; :: thesis: verum

end;

end;