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, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds
(rng T) /\ (rng S) = {}
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, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds
(rng T) /\ (rng S) = {}
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, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds
(rng T) /\ (rng S) = {}
let q be FinSequence of NAT ; :: thesis: ( Tseq,q,p is_constructingBinHuffmanTree implies for i being Nat
for T, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds
(rng T) /\ (rng S) = {} )
assume A1: Tseq,q,p is_constructingBinHuffmanTree ; :: thesis: for i being Nat
for T, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds
(rng T) /\ (rng S) = {}
defpred S₂[ Nat] means ( 1 <= $1 & $1 <= len Tseq implies for T, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . $1 & S in Tseq . $1 & T <> S holds
(rng T) /\ (rng S) = {} );
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, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . (i + 1) & S in Tseq . (i + 1) & T <> S holds
(rng T) /\ (rng S) = {}
let d, h be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( d in Tseq . (i + 1) & h in Tseq . (i + 1) & d <> h implies (rng d) /\ (rng h) = {} )
assume A6: ( d in Tseq . (i + 1) & h in Tseq . (i + 1) & d <> h ) ; :: thesis: (rng d) /\ (rng h) = {}

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

suppose A7: i = 0 ; :: thesis: (rng d) /\ (rng h) = {}

then consider d0 being Element of FinTrees IndexedREAL such that
A8: ( 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;
consider x being Element of SOURCE such that
A9: d0 = root-tree [(((canFS SOURCE) ") . x),(p . {x})] by A8;
consider h0 being Element of FinTrees IndexedREAL such that
A10: ( h0 = h & h0 is finite binary DecoratedTree of IndexedREAL & ex y being Element of SOURCE st h0 = root-tree [(((canFS SOURCE) ") . y),(p . {y})] ) by A7, A1, A6;
consider y being Element of SOURCE such that
A11: h0 = root-tree [(((canFS SOURCE) ") . y),(p . {y})] by A10;
thus (rng d) /\ (rng h) = {} :: thesis: verum

proof

assume (rng d) /\ (rng h) <> {} ; :: thesis: contradiction
then consider z being object such that
A12: z in (rng d) /\ (rng h) by XBOOLE_0:def 1;
A13: ( z in rng d & z in rng h ) by XBOOLE_0:def 4, A12;
A14: rng d = {[(((canFS SOURCE) ") . x),(p . {x})]} by A8, A9, FUNCOP_1:8;
A15: rng h = {[(((canFS SOURCE) ") . y),(p . {y})]} by A10, A11, FUNCOP_1:8;
[(((canFS SOURCE) ") . x),(p . {x})] = z by TARSKI:def 1, A14, A13
.= [(((canFS SOURCE) ") . y),(p . {y})] by TARSKI:def 1, A15, A13 ;
hence contradiction by A6, A8, A10, A9, A11; :: thesis: verum

end;

end;

suppose A16: i <> 0 ; :: thesis: (rng d) /\ (rng h) = {}

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
A17: ( 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;
A18: for T being finite binary DecoratedTree of IndexedREAL st T in X holds
for p being Element of dom T
for r being Element of NAT st r = (T . p) `1 holds
r <= MaxVl X by A1, A17, Th26;
A19: ( w = MakeTree (t,s,((MaxVl X) + 1)) or w = MakeTree (s,t,((MaxVl X) + 1)) ) by A17, TARSKI:def 2;
A20: ( s in X & t in Y ) by Def10;
then ( t in X & not t in {s} ) by A17, XBOOLE_0:def 5;
then A21: ( t in X & t <> s ) by TARSKI:def 1;

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

suppose ( d in X \ {t,s} & h in X \ {t,s} ) ; :: thesis: (rng d) /\ (rng h) = {}

then ( d in Tseq . i & h in Tseq . i ) by A17, XBOOLE_0:def 5;
hence (rng d) /\ (rng h) = {} by A16, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A4, A6; :: thesis: verum

end;

suppose ( d in {w} & h in X \ {t,s} ) ; :: thesis: (rng d) /\ (rng h) = {}

then ( d = w & h in X \ {t,s} ) by TARSKI:def 1;
hence (rng d) /\ (rng h) = {} by A20, A19, A17, A16, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A4, A18, A21, Th28; :: thesis: verum

end;

suppose ( d in X \ {t,s} & h in {w} ) ; :: thesis: (rng d) /\ (rng h) = {}

then ( d in X \ {t,s} & h = w ) by TARSKI:def 1;
hence (rng d) /\ (rng h) = {} by A20, A19, A16, A5, XXREAL_0:2, NAT_1:16, NAT_1:14, A4, A18, A17, A21, Th28; :: thesis: verum

end;

suppose ( d in {w} & h in {w} ) ; :: thesis: (rng d) /\ (rng h) = {}

then ( d = w & h = w ) by TARSKI:def 1;
hence (rng d) /\ (rng h) = {} by A6; :: thesis: verum

end;

end;

end;

end;

end;

A22: for i being Nat holds S₂[i] from NAT_1:sch 2(A2, A3);
let i be Nat; :: thesis: for T, S being finite binary DecoratedTree of IndexedREAL st T in Tseq . i & S in Tseq . i & T <> S holds
(rng T) /\ (rng S) = {}
let T, S be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( T in Tseq . i & S in Tseq . i & T <> S implies (rng T) /\ (rng S) = {} )
assume A23: ( T in Tseq . i & S in Tseq . i & T <> S ) ; :: thesis: (rng T) /\ (rng S) = {}
i in dom Tseq by A23, FUNCT_1:def 2;
then ( 1 <= i & i <= len Tseq ) by FINSEQ_3:25;
hence (rng T) /\ (rng S) = {} by A23, A22; :: thesis: verum