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 T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
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 T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
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 T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
let q be FinSequence of NAT ; :: thesis: ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one )
assume A1: Tseq,q,p is_constructingBinHuffmanTree ; :: thesis: for i being Nat
for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= len Tseq implies for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . $1 holds
T is one-to-one );
A2: S₂[ 0 ] ;
A3: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A4: S₂[i] ; :: thesis: S₂[i + 1]
assume A5: ( 1 <= i + 1 & i + 1 <= len Tseq ) ; :: thesis: for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . (i + 1) holds
T is one-to-one
let d be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( d in Tseq . (i + 1) implies d is one-to-one )
assume A6: d in Tseq . (i + 1) ; :: thesis: d is one-to-one

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: d is one-to-one

then ex d0 being Element of FinTrees IndexedREAL st
( d0 = d & d0 is finite binary DecoratedTree of IndexedREAL & ex x being Element of SOURCE st d0 = root-tree [(((canFS SOURCE) ") . x),(p . {x})] ) by A1, A6;
hence d is one-to-one ; :: thesis: verum

end;

suppose A7: i <> 0 ; :: thesis: d is one-to-one

then ( 1 <= i & i < len Tseq ) by A5, XXREAL_0:2, NAT_1:16, NAT_1:14;
then 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
A8: ( Tseq . i = X & Y = X \ {s} & w in {(MakeTree (t,s,((MaxVl X) + 1))),(MakeTree (s,t,((MaxVl X) + 1)))} & Tseq . (i + 1) = (X \ {t,s}) \/ {w} ) by A1;
A9: ( w = MakeTree (t,s,((MaxVl X) + 1)) or w = MakeTree (s,t,((MaxVl X) + 1)) ) by A8, TARSKI:def 2;
A10: ( s in X & t in Y ) by Def10;
then A11: ( t in X & not t in {s} ) by A8, XBOOLE_0:def 5;
then A12: ( t in X & t <> s ) by TARSKI:def 1;
A13: for z being finite binary DecoratedTree of IndexedREAL st z in X holds
not [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] in rng z by A10, A1, Th27, A8, A11;
A14: ( s is one-to-one & t is one-to-one ) by A10, A11, A8, A4, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A7;
A15: (rng s) /\ (rng t) = {} by A10, A12, A8, Th29, A1;

per cases ( d in X \ {t,s} or d in {w} ) by XBOOLE_0:def 3, A8, A6;

suppose d in X \ {t,s} ; :: thesis: d is one-to-one

then ( d in X & not d in {t,s} ) by XBOOLE_0:def 5;
hence d is one-to-one by A7, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A4, A8; :: thesis: verum

end;

suppose A16: d in {w} ; :: thesis: d is one-to-one

per cases ( d = MakeTree (t,s,((MaxVl X) + 1)) or d = MakeTree (s,t,((MaxVl X) + 1)) ) by A16, TARSKI:def 1, A9;

suppose d = MakeTree (t,s,((MaxVl X) + 1)) ; :: thesis: d is one-to-one

hence d is one-to-one by A10, Th30, A13, A11, A14, A15; :: thesis: verum

end;

suppose d = MakeTree (s,t,((MaxVl X) + 1)) ; :: thesis: d is one-to-one

hence d is one-to-one by A10, Th30, A13, A11, A14, A15; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

A17: for i being Nat holds S₂[i] from NAT_1:sch 2(A2, A3);
let i be Nat; :: thesis: for T being finite binary DecoratedTree of IndexedREAL st T in Tseq . i holds
T is one-to-one
let T be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( T in Tseq . i implies T is one-to-one )
assume A18: T in Tseq . i ; :: thesis: T is one-to-one
i in dom Tseq by A18, FUNCT_1:def 2;
then ( 1 <= i & i <= len Tseq ) by FINSEQ_3:25;
hence T is one-to-one by A18, A17; :: thesis: verum