let X be non empty finite Subset of (BinFinTrees IndexedREAL); for s, t, w being finite binary DecoratedTree of IndexedREAL st ( 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 ) & ( for p, q being finite binary DecoratedTree of IndexedREAL st p in X & q in X & p <> q holds
(rng p) /\ (rng q) = {} ) & s in X & t in X & s <> t & w in X \ {s,t} holds
(rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) = {}
let s, t, w be finite binary DecoratedTree of IndexedREAL ; ( ( 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 ) & ( for p, q being finite binary DecoratedTree of IndexedREAL st p in X & q in X & p <> q holds
(rng p) /\ (rng q) = {} ) & s in X & t in X & s <> t & w in X \ {s,t} implies (rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) = {} )
assume A1:
( ( 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 ) & ( for p, q being finite binary DecoratedTree of IndexedREAL st p in X & q in X & p <> q holds
(rng p) /\ (rng q) = {} ) & s in X & t in X & s <> t & w in X \ {s,t} )
; (rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) = {}
set d = MakeTree (t,s,((MaxVl X) + 1));
A2:
(MakeTree (t,s,((MaxVl X) + 1))) . {} = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))]
by TREES_4:def 4;
set bx = [((MaxVl X) + 1),((Vrootr t) + (Vrootr s))];
set q = <*(dom t),(dom s)*>;
A3:
len <*(dom t),(dom s)*> = 2
by FINSEQ_1:44;
A4:
<*(dom t),(dom s)*> . 1 = dom t
by FINSEQ_1:44;
A5:
<*(dom t),(dom s)*> . 2 = dom s
by FINSEQ_1:44;
A6:
dom ([((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] -tree (t,s)) = tree ((dom t),(dom s))
by TREES_4:14;
A7:
for a being object holds
( not a in dom (MakeTree (t,s,((MaxVl X) + 1))) or a = {} or ex f being Element of dom t st a = <*0*> ^ f or ex f being Element of dom s st a = <*1*> ^ f )
assume
(rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) <> {}
; contradiction
then consider nx being object such that
A10:
nx in (rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w)
by XBOOLE_0:def 1;
A11:
( nx in rng (MakeTree (t,s,((MaxVl X) + 1))) & nx in rng w )
by XBOOLE_0:def 4, A10;
then consider a0 being object such that
A12:
( a0 in dom (MakeTree (t,s,((MaxVl X) + 1))) & nx = (MakeTree (t,s,((MaxVl X) + 1))) . a0 )
by FUNCT_1:def 3;
consider b0 being object such that
A13:
( b0 in dom w & nx = w . b0 )
by FUNCT_1:def 3, A11;
reconsider a = a0 as Element of dom (MakeTree (t,s,((MaxVl X) + 1))) by A12;
reconsider b = b0 as Element of dom w by A13;
A14:
( w in X & w <> s & w <> t )
then A15:
(rng s) /\ (rng w) = {}
by A1;
A16:
(rng t) /\ (rng w) = {}
by A1, A14;
ex x, y being object st
( x in NAT & y in REAL & w . b = [x,y] )
by ZFMISC_1:def 2;
then reconsider r = (w . b) `1 as Element of NAT ;