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;

per cases ( x1 = 0. ((dim p) -chain-space p) or x2 = 0. ((dim p) -chain-space p) ) by A4, Th67;

suppose x1 = 0. ((dim p) -chain-space p) ; :: thesis: contradiction

then ( x2 = {p} & ((dim p) -boundary p) . x1 = 0. (((dim p) - 1) -chain-space p) ) by A4, Th66, RANKNULL:9;
hence contradiction by A3, Th74; :: thesis: verum

end;

suppose x2 = 0. ((dim p) -chain-space p) ; :: thesis: contradiction

then ( x1 = {p} & ((dim p) -boundary p) . x2 = 0. (((dim p) - 1) -chain-space p) ) by A4, Th66, RANKNULL:9;
hence contradiction by A3, Th74; :: thesis: verum

end;

end;