let X be non empty finite Subset of (BinFinTrees 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 ) implies for s, t, w being finite binary DecoratedTree of IndexedREAL st s in X & t in X & w = MakeTree (t,s,((MaxVl X) + 1)) holds
for p being Element of dom w
for r being Element of NAT st r = (w . p) `1 holds
r <= (MaxVl X) + 1 )
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 ; :: thesis: for s, t, w being finite binary DecoratedTree of IndexedREAL st s in X & t in X & w = MakeTree (t,s,((MaxVl X) + 1)) holds
for p being Element of dom w
for r being Element of NAT st r = (w . p) `1 holds
r <= (MaxVl X) + 1
let s, t, d be finite binary DecoratedTree of IndexedREAL ; :: thesis: ( s in X & t in X & d = MakeTree (t,s,((MaxVl X) + 1)) implies for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= (MaxVl X) + 1 )
assume A2: ( s in X & t in X & d = MakeTree (t,s,((MaxVl X) + 1)) ) ; :: thesis: for p being Element of dom d
for r being Element of NAT st r = (d . p) `1 holds
r <= (MaxVl X) + 1
then A3: d . {} = [((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)*>;
A4: len <*(dom t),(dom s)*> = 2 by FINSEQ_1:44;
A7: dom ([((MaxVl X) + 1),((Vrootr t) + (Vrootr s))] -tree (t,s)) = tree ((dom t),(dom s)) by TREES_4:14;
A8: for a being object holds
( not a in dom d 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 d 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 A9: a in dom d ; :: 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 A9, A2, A7, 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
A10: ( 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, A10, A4;

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 A10; :: 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 A10; :: thesis: verum

end;

end;

end;

end;

end;

let a be Element of dom d; :: thesis: for r being Element of NAT st r = (d . a) `1 holds
r <= (MaxVl X) + 1
let r be Element of NAT ; :: thesis: ( r = (d . a) `1 implies r <= (MaxVl X) + 1 )
assume A11: r = (d . a) `1 ; :: thesis: r <= (MaxVl X) + 1

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 A8;

suppose a = {} ; :: thesis: r <= (MaxVl X) + 1

hence r <= (MaxVl X) + 1 by A11, A3; :: thesis: verum

end;

suppose ex f being Element of dom t st a = <*0*> ^ f ; :: thesis: r <= (MaxVl X) + 1

then consider f being Element of dom t such that
A12: a = <*0*> ^ f ;
A13: (d . a) `1 = (t . f) `1 by A12, Th11, A2;
ex x, y being object st
( x in NAT & y in REAL & t . f = [x,y] ) by ZFMISC_1:def 2;
then reconsider q = (t . f) `1 as Element of NAT ;
q <= MaxVl X by A1, A2;
hence r <= (MaxVl X) + 1 by A11, A13, NAT_1:16, XXREAL_0:2; :: thesis: verum

end;

suppose ex f being Element of dom s st a = <*1*> ^ f ; :: thesis: r <= (MaxVl X) + 1

then consider f being Element of dom s such that
A14: a = <*1*> ^ f ;
A15: (d . a) `1 = (s . f) `1 by A14, Th12, A2;
ex x, y being object st
( x in NAT & y in REAL & s . f = [x,y] ) by ZFMISC_1:def 2;
then reconsider q = (s . f) `1 as Element of NAT ;
q <= MaxVl X by A1, A2;
hence r <= (MaxVl X) + 1 by A11, A15, NAT_1:16, XXREAL_0:2; :: thesis: verum

end;

end;