theorem :: HUFFMAN1:20

for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for T being BinHuffmanTree of p holds Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }