let p be polyhedron; :: thesis: for k being Integer st - 1 <= k & k <= dim p holds
for m, n being Nat st 1 <= n & n <= num-polytopes p,k & 1 <= m & m <= num-polytopes p,k & n -th-polytope p,k = m -th-polytope p,k holds
m = n
let k be Integer; :: thesis: ( - 1 <= k & k <= dim p implies for m, n being Nat st 1 <= n & n <= num-polytopes p,k & 1 <= m & m <= num-polytopes p,k & n -th-polytope p,k = m -th-polytope p,k holds
m = n )
assume A1: ( - 1 <= k & k <= dim p ) ; :: thesis: for m, n being Nat st 1 <= n & n <= num-polytopes p,k & 1 <= m & m <= num-polytopes p,k & n -th-polytope p,k = m -th-polytope p,k holds
m = n
let m, n be Nat; :: thesis: ( 1 <= n & n <= num-polytopes p,k & 1 <= m & m <= num-polytopes p,k & n -th-polytope p,k = m -th-polytope p,k implies m = n )
assume that
A2: 1 <= n and
A3: n <= num-polytopes p,k and
A4: 1 <= m and
A5: m <= num-polytopes p,k and
A6: n -th-polytope p,k = m -th-polytope p,k ; :: thesis: m = n
set s = k -polytope-seq p;
A7: n -th-polytope p,k = (k -polytope-seq p) . n by A1, A2, A3, Def12;
A8: m -th-polytope p,k = (k -polytope-seq p) . m by A1, A4, A5, Def12;
n in Seg (num-polytopes p,k) by A2, A3, FINSEQ_1:3;
then A9: n in dom (k -polytope-seq p) by Th28;
m in Seg (num-polytopes p,k) by A4, A5, FINSEQ_1:3;
then A10: m in dom (k -polytope-seq p) by Th28;
k -polytope-seq p is one-to-one by Th34;
hence m = n by A6, A7, A8, A9, A10, FUNCT_1:def 8; :: thesis: verum