let p be polyhedron; for k being Integer st - 1 <= k & k <= dim p holds
for x being Element of k -polytopes p ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
let k be Integer; ( - 1 <= k & k <= dim p implies for x being Element of k -polytopes p ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) ) )
assume A1:
( - 1 <= k & k <= dim p )
; for x being Element of k -polytopes p ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
let x be Element of k -polytopes p; ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
per cases
( k = - 1 or k = dim p or ( - 1 < k & k < dim p ) )
by A1, XXREAL_0:1;
suppose A6:
(
- 1
< k &
k < dim p )
;
ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )set F = the
PolytopsF of
p;
A7:
k -polytopes p = rng ( the PolytopsF of p . (k + 1))
by A6, Def5;
A8:
(- 1) + 1
< k + 1
by A6, XREAL_1:6;
then A9:
0 + 1
<= k + 1
by INT_1:7;
reconsider k9 =
k + 1 as
Element of
NAT by A8, INT_1:3;
k + 1
<= dim p
by A6, INT_1:7;
then
not the
PolytopsF of
p . k9 is
empty
by A9, Def3;
then consider m being
object such that A10:
m in dom ( the PolytopsF of p . k9)
and A11:
( the PolytopsF of p . k9) . m = x
by A7, FUNCT_1:def 3;
reconsider Fk9 = the
PolytopsF of
p . k9 as
FinSequence ;
reconsider m =
m as
Element of
NAT by A10;
dom Fk9 = Seg (len Fk9)
by FINSEQ_1:def 3;
then A12:
( 1
<= m &
m <= len Fk9 )
by A10, FINSEQ_1:1;
take
m
;
( x = m -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) )A13:
k -polytope-seq p = the
PolytopsF of
p . (k + 1)
by A6, Def7;
then
num-polytopes (
p,
k)
= len ( the PolytopsF of p . (k + 1))
by Th26;
hence
(
x = m -th-polytope (
p,
k) & 1
<= m &
m <= num-polytopes (
p,
k) )
by A13, A11, A12, Def12;
verum end;