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
for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
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
for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
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
for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
let q be FinSequence of NAT ; :: thesis: ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat
for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z )
assume A1: Tseq,q,p is_constructingBinHuffmanTree ; :: thesis: for i being Nat
for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
let i be Nat; :: thesis: for s, t being finite binary DecoratedTree of IndexedREAL
for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
let s, t be finite binary DecoratedTree of IndexedREAL ; :: thesis: for X being non empty finite Subset of (BinFinTrees IndexedREAL) st X = Tseq . i & s in X & t in X holds
for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: ( X = Tseq . i & s in X & t in X implies for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z )
assume A2: ( X = Tseq . i & s in X & t in X ) ; :: thesis: for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
let z be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( z in X implies not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z )
assume A3: z in X ; :: thesis: not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z
assume [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z ; :: thesis: contradiction
then consider p0 being object such that
A4: ( p0 in dom z & [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] = z . p0 ) by FUNCT_1:def 3;
reconsider p0 = p0 as Element of dom z by A4;
ex x, y being object st
( x in NAT & y in REAL & z . p0 = [x,y] ) by ZFMISC_1:def 2;
then reconsider r = (z . p0) `1 as Element of NAT ;
r = (MaxVl X) + 1 by A4;
hence contradiction by NAT_1:16, A3, Th26, A1, A2; :: thesis: verum