theorem Th11: :: HUFFMAN1:11

for s, t being DecoratedTree
for x being object
for q being FinSequence of NAT st q in dom t holds
(x -tree (t,s)) . (<*0*> ^ q) = t . q