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
for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1
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
for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1
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
for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1
let q be FinSequence of NAT ; :: thesis: ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat st 1 <= i & i < len Tseq holds
for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1 )
assume A1: Tseq,q,p is_constructingBinHuffmanTree ; :: thesis: for i being Nat st 1 <= i & i < len Tseq holds
for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1
let i be Nat; :: thesis: ( 1 <= i & i < len Tseq implies for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1 )
assume ( 1 <= i & i < len Tseq ) ; :: thesis: for X, Y being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & Y = Tseq . (i + 1) holds
MaxVl Y = (MaxVl X) + 1
then consider X, Y being non empty finite Subset of (BinFinTrees IndexedREAL), s being MinValueTree of X, t being MinValueTree of Y, v being finite binary DecoratedTree of IndexedREAL such that
A2: ( Tseq . i = X & Y = X \ {s} & v in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (i + 1) = (X \ {t,s}) \/ {v} ) by A1;
let X0, Y0 be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: ( X0 = Tseq . i & Y0 = Tseq . (i + 1) implies MaxVl Y0 = (MaxVl X0) + 1 )
assume A3: ( X0 = Tseq . i & Y0 = Tseq . (i + 1) ) ; :: thesis: MaxVl Y0 = (MaxVl X0) + 1
consider LX0 being non empty finite Subset of NAT such that
A4: ( LX0 = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X0 } & MaxVl X0 = max LX0 ) by Def9;
consider LY0 being non empty finite Subset of NAT such that
A5: ( LY0 = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in Y0 } & MaxVl Y0 = max LY0 ) by Def9;
( v = [((MaxVl X0) + 1),((Vrootr t) + (Vrootr s))] -tree (t,s) or v = [((MaxVl X0) + 1),((Vrootr s) + (Vrootr t))] -tree (s,t) ) by TARSKI:def 2, A2, A3;
then A6: ( v . {} = [((MaxVl X0) + 1),((Vrootr t) + (Vrootr s))] or v . {} = [((MaxVl X0) + 1),((Vrootr s) + (Vrootr t))] ) by TREES_4:def 4;
( dom v is finite & dom v is binary ) by BINTREE1:def 3;
then reconsider pv = v as Element of BinFinTrees IndexedREAL by Def2;
v in {v} by TARSKI:def 1;
then v in Tseq . (i + 1) by A2, XBOOLE_0:def 3;
then A7: Vrootl pv in LY0 by A5, A3;
for x being ExtReal st x in LY0 holds
x <= Vrootl pv

proof

let x be ExtReal; :: thesis: ( x in LY0 implies x <= Vrootl pv )
assume x in LY0 ; :: thesis: x <= Vrootl pv
then consider p being Element of BinFinTrees IndexedREAL such that
A8: ( x = Vrootl p & p in Y0 ) by A5;
A9: ( p in X \ {t,s} or p in {v} ) by XBOOLE_0:def 3, A8, A3, A2;

per cases ( p in X0 or p = v ) by A9, TARSKI:def 1, A3, A2, XBOOLE_0:def 5;

suppose p in X0 ; :: thesis: x <= Vrootl pv

then Vrootl p in LX0 by A4;
then Vrootl p <= MaxVl X0 by A4, XXREAL_2:def 8;
hence x <= Vrootl pv by A6, A8, NAT_1:16, XXREAL_0:2; :: thesis: verum

end;

suppose p = v ; :: thesis: x <= Vrootl pv

hence x <= Vrootl pv by A8; :: thesis: verum

end;

end;

end;

hence MaxVl Y0 = (MaxVl X0) + 1 by A5, A6, A7, XXREAL_2:def 8; :: thesis: verum