for SOURCE being non empty finite set
for p being Probability of Trivial-SigmaField SOURCE
for Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat
for T, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds
(rng T) /\ (rng S) = {}