theorem :: HUFFMAN1:22

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for T being BinHuffmanTree of p
for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)