let SOURCE be non empty finite set ; :: thesis: for p being Probability of Trivial-SigmaField SOURCE
for T being BinHuffmanTree of p
for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
let p be Probability of Trivial-SigmaField SOURCE; :: thesis: for T being BinHuffmanTree of p
for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
let T be BinHuffmanTree of p; :: thesis: for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r)
A1: ex Tseq being FinSequence of BoolBinFinTrees IndexedREAL ex q being FinSequence of NAT st
( Tseq,q,p is_constructingBinHuffmanTree & {T} = Tseq . (len Tseq) ) by Def13;
T in {T} by TARSKI:def 1;
hence for t, s, r being Element of dom T st t in (dom T) \ (Leaves (dom T)) & s = t ^ <*0*> & r = t ^ <*1*> holds
Vtree t = (Vtree s) + (Vtree r) by A1, Th21; :: thesis: verum