theorem Th21: :: HUFFMAN1:21

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for T being finite binary DecoratedTree of IndexedREAL
for t, s, r being Element of dom T st T in Tseq . i & t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)