let SOURCE be non empty finite set ; :: thesis: 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 st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { 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 Tseq being FinSequence of BoolBinFinTrees IndexedREAL
for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let Tseq be FinSequence of BoolBinFinTrees IndexedREAL; :: thesis: for q being FinSequence of NAT st Tseq,q,p is_constructingBinHuffmanTree holds
for i being Nat st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
let q be FinSequence of NAT ; :: thesis: ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } )
assume A1: Tseq,q,p is_constructingBinHuffmanTree ; :: thesis: for i being Nat st 1 <= i & i <= len Tseq holds
union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
defpred S2[ Nat] means ( $1 < len Tseq implies union (LeavesSet (Tseq . ($1 + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } );
A2: S2[ 0 ] by Th18, A1;
A3: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A4: S2[k] ; :: thesis: S2[k + 1]
assume A5: k + 1 < len Tseq ; :: thesis: union (LeavesSet (Tseq . ((k + 1) + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
A6: k <= k + 1 by NAT_1:11;
consider X, Y being non empty finite Subset of (BinFinTrees IndexedREAL), s being MinValueTree of X, t being MinValueTree of Y, w being finite binary DecoratedTree of IndexedREAL such that
A7: ( Tseq . (k + 1) = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . ((k + 1) + 1) = (X \ {t,s}) \/ {w} ) by A1, A5, NAT_1:11;
A8: ( w = MakeTree (t,s,((MaxVl X) + 1)) or w = MakeTree (s,t,((MaxVl X) + 1)) ) by A7, TARSKI:def 2;
A9: LeavesSet (Tseq . ((k + 1) + 1)) = (LeavesSet (X \ {t,s})) \/ (LeavesSet {w}) by Th8, A7;
A10: union (LeavesSet {w}) = union (LeavesSet {t,s}) by Th14, A8;
A11: union (LeavesSet (Tseq . ((k + 1) + 1))) = (union (LeavesSet (X \ {t,s}))) \/ (union (LeavesSet {w})) by ZFMISC_1:78, A9
.= union ((LeavesSet (X \ {t,s})) \/ (LeavesSet {t,s})) by ZFMISC_1:78, A10
.= union (LeavesSet ((X \ {t,s}) \/ {t,s})) by Th8 ;
A12: ( s in X & t in Y ) by Def10;
then ( t in X & not t in {s} ) by A7, XBOOLE_0:def 5;
hence union (LeavesSet (Tseq . ((k + 1) + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } by A12, A6, A4, A5, XXREAL_0:2, A7, A11, XBOOLE_1:45, ZFMISC_1:32; :: thesis: verum
end;
A13: for k being Nat holds S2[k] from NAT_1:sch 2(A2, A3);
 let i be Nat; :: thesis: ( 1 <= i & i <= len Tseq implies union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } )
assume A14: ( 1 <= i & i <= len Tseq ) ; :: thesis: union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] }
then reconsider i1 = i - 1 as Nat by NAT_1:21;
i - 1 < (len Tseq) - 0 by XREAL_1:15, A14;
then union (LeavesSet (Tseq . (i1 + 1))) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } by A13;
hence union (LeavesSet (Tseq . i)) = { z where z is Element of [:NAT,REAL:] : ex x being Element of SOURCE st z = [(((canFS SOURCE) ") . x),(p . {x})] } ; :: thesis: verum