let p be polyhedron; :: thesis: for k being Integer
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: 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
A1: ( 1 <= n & n <= num-polytopes (p,k) ) and
A2: ( 1 <= m & m <= num-polytopes (p,k) ) and
A3: n -th-polytope (p,k) = m -th-polytope (p,k) ; :: thesis: m = n
set s = k -polytope-seq p;
A4: k -polytope-seq p is one-to-one by Th31;
m in Seg (num-polytopes (p,k)) by A2;
then A5: m in dom (k -polytope-seq p) by Th25;
n in Seg (num-polytopes (p,k)) by A1;
then A6: n in dom (k -polytope-seq p) by Th25;
( n -th-polytope (p,k) = (k -polytope-seq p) . n & m -th-polytope (p,k) = (k -polytope-seq p) . m ) by A1, A2, Def12;
hence m = n by A3, A6, A5, A4, FUNCT_1:def 4; :: thesis: verum