let X be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis: 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 ; :: thesis: ( ( 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} ) ; :: thesis: (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;
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 )

proof

let a be object ; :: thesis: ( 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 A8: a in dom (MakeTree (t,s,((MaxVl X) + 1))) ; :: thesis: ( 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 )

per cases ( a = {} or ex n being Nat ex f being FinSequence st
( n < len <*(dom t),(dom s)*> & f in <*(dom t),(dom s)*> . (n + 1) & a = <*n*> ^ f ) ) by A8, A6, TREES_3:def 15;

suppose a = {} ; :: thesis: ( 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 )

hence ( 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 ) ; :: thesis: verum

end;

suppose ex n being Nat ex f being FinSequence st
( n < len <*(dom t),(dom s)*> & f in <*(dom t),(dom s)*> . (n + 1) & a = <*n*> ^ f ) ; :: thesis: ( 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 )

then consider n being Nat, f being FinSequence such that
A9: ( n < len <*(dom t),(dom s)*> & f in <*(dom t),(dom s)*> . (n + 1) & a = <*n*> ^ f ) ;

per cases ( n = 0 or n = 1 ) by NAT_1:23, A3, A9;

suppose n = 0 ; :: thesis: ( 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 )

hence ( 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 ) by A9; :: thesis: verum

end;

suppose n = 1 ; :: thesis: ( 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 )

hence ( 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 ) by A9; :: thesis: verum

end;

end;

end;

end;

end;

assume (rng (MakeTree (t,s,((MaxVl X) + 1)))) /\ (rng w) <> {} ; :: thesis: 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 )

proof

( w in X & not w in {s,t} ) by A1, XBOOLE_0:def 5;
hence ( w in X & w <> s & w <> t ) by TARSKI:def 2; :: thesis: verum

end;

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 ;

per cases ( 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 ) by A7;

suppose a = {} ; :: thesis: contradiction

then ((MakeTree (t,s,((MaxVl X) + 1))) . a) `1 = (MaxVl X) + 1 by A2;
hence contradiction by NAT_1:16, A1, A14, A12, A13; :: thesis: verum

end;

suppose ex f being Element of dom t st a = <*0*> ^ f ; :: thesis: contradiction

then consider f being Element of dom t such that
A17: a = <*0*> ^ f ;
(MakeTree (t,s,((MaxVl X) + 1))) . a = t . f by A17, Th11;
then (MakeTree (t,s,((MaxVl X) + 1))) . a in rng t by FUNCT_1:3;
hence contradiction by A16, A12, A11, XBOOLE_0:def 4; :: thesis: verum

end;

suppose ex f being Element of dom s st a = <*1*> ^ f ; :: thesis: contradiction

then consider f being Element of dom s such that
A18: a = <*1*> ^ f ;
(MakeTree (t,s,((MaxVl X) + 1))) . a = s . f by A18, Th12;
then nx in rng s by A12, FUNCT_1:3;
hence contradiction by A15, A11, XBOOLE_0:def 4; :: thesis: verum

end;

end;