theorem Th17: :: HUFFMAN1:17

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree