let p be polyhedron; :: thesis: (dim p) -boundary p is one-to-one
set T = (dim p) -boundary p;
set U = ((dim p) - 1) -chain-space p;
set V = (dim p) -chain-space p;
set B = {p};
assume not (dim p) -boundary p is one-to-one ; :: thesis: contradiction
then consider x1, x2 being object such that
A1: x1 in dom ((dim p) -boundary p) and
A2: x2 in dom ((dim p) -boundary p) and
A3: ((dim p) -boundary p) . x1 = ((dim p) -boundary p) . x2 and
A4: x1 <> x2 by FUNCT_1:def 4;
reconsider x2 = x2 as Element of ((dim p) -chain-space p) by A2;
reconsider x1 = x1 as Element of ((dim p) -chain-space p) by A1;