ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree by Th17;
hence ex b₁ being finite binary DecoratedTree of IndexedREAL ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st
( Tseq,q,p is_constructingBinHuffmanTree & {b₁} = Tseq . (len Tseq) ) ; :: thesis: verum