let p be polyhedron; :: thesis: for k being Integer holds rng (k -polytope-seq p) = k -polytopes p
let k be Integer; :: thesis: rng (k -polytope-seq p) = k -polytopes p
set F = the PolytopsF of p;

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

suppose A1: k < - 1 ; :: thesis: rng (k -polytope-seq p) = k -polytopes p

then k -polytopes p = {} by Def5;
hence rng (k -polytope-seq p) = k -polytopes p by A1, Def7, RELAT_1:38; :: thesis: verum

end;

suppose A2: ( - 1 <= k & k <= dim p ) ; :: thesis: rng (k -polytope-seq p) = k -polytopes p

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

suppose k = - 1 ; :: thesis: rng (k -polytope-seq p) = k -polytopes p

then ( k -polytopes p = {{}} & k -polytope-seq p = <*{}*> ) by Def5, Def7;
hence rng (k -polytope-seq p) = k -polytopes p by FINSEQ_1:38; :: thesis: verum

end;

suppose A3: ( - 1 < k & k < dim p ) ; :: thesis: rng (k -polytope-seq p) = k -polytopes p

then k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by Def5;
hence rng (k -polytope-seq p) = k -polytopes p by A3, Def7; :: thesis: verum

end;

suppose k = dim p ; :: thesis: rng (k -polytope-seq p) = k -polytopes p

then ( k -polytopes p = {p} & k -polytope-seq p = <*p*> ) by Def5, Def7;
hence rng (k -polytope-seq p) = k -polytopes p by FINSEQ_1:38; :: thesis: verum

end;

end;

end;

suppose A4: k > dim p ; :: thesis: rng (k -polytope-seq p) = k -polytopes p

then k -polytopes p = {} by Def5;
hence rng (k -polytope-seq p) = k -polytopes p by A4, Def7, RELAT_1:38; :: thesis: verum

end;

end;