theorem Th14: :: HUFFMAN1:14

for k being Nat
for s, t being finite binary DecoratedTree of IndexedREAL holds union (LeavesSet {s,t}) = union (LeavesSet {(MakeTree (t,s,k))})