theorem Th23: :: HUFFMAN1:23

for X being non empty finite Subset of (BinFinTrees IndexedREAL) st ( for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X ) holds
for s, t, w being finite binary DecoratedTree of IndexedREAL st s in X & t in X & w = MakeTree (t,s,((MaxVl X) + 1)) holds
for p being Element of dom w
for r being Element of NAT st r = (w . p) `1 holds
r <= (MaxVl X) + 1