let T be BinHuffmanTree of p; :: thesis: T is one-to-one
A1: ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st
( Tseq,q,p is_constructingBinHuffmanTree & {T} = Tseq . (len Tseq) ) by Def13;
T in {T} by TARSKI:def 1;
hence T is one-to-one by A1, Th31; :: thesis: verum