let SOURCE be non empty finite set ; :: thesis: for p being Probability of Trivial-SigmaField SOURCE
for T being BinHuffmanTree of p holds Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let p be Probability of Trivial-SigmaField SOURCE; :: thesis: for T being BinHuffmanTree of p holds Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let T be BinHuffmanTree of p; :: thesis: Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
consider Tseq being FinSequence of BoolBinFinTrees IndexedREAL, q being FinSequence of NAT such that
A1: ( Tseq,q,p is_constructingBinHuffmanTree & {T} = Tseq . (len Tseq) ) by Def13;
1 <= len Tseq by NAT_1:14, A1;
then A2: union (LeavesSet {T}) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } by Th19, A1;
LeavesSet {T} = {(Leaves T)} by Th7;
hence Leaves T = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } by A2, ZFMISC_1:25; :: thesis: verum