theorem Th12: :: HUFFMAN1:12

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