theorem Th18: :: HUFFMAN1:18

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