let X, Y, Z be non empty finite Subset of (BinFinTrees IndexedREAL); :: thesis:
assume A1: Z = X \/ Y ; :: thesis:
set mz = MaxVl Z;
consider L being non empty finite Subset of NAT such that
A2: ( L = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in Z } & MaxVl Z = max L ) by Def9;
( MaxVl Z in L & ( for b being Nat st b in L holds
b <= MaxVl Z ) ) by XXREAL_2:def 8, A2;
then consider p being Element of BinFinTrees IndexedREAL such that
A3: ( MaxVl Z = Vrootl p & p in Z ) by A2;
consider LX being non empty finite Subset of NAT such that
A4: ( LX = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in X } & MaxVl X = max LX ) by Def9;
( max LX in LX & ( for x being Nat st x in LX holds
x <= max LX ) ) by XXREAL_2:def 8;
then consider px being Element of BinFinTrees IndexedREAL such that
A5: ( max LX = Vrootl px & px in X ) by A4;
px in Z by A5, A1, XBOOLE_0:def 3;
then Vrootl px in L by A2;
then A6: max LX <= MaxVl Z by A5, XXREAL_2:def 8, A2;
consider LY being non empty finite Subset of NAT such that
A7: ( LY = { (Vrootl p) where p is Element of BinFinTrees IndexedREAL : p in Y } & MaxVl Y = max LY ) by Def9;
( max LY in LY & ( for y being Nat st y in LY holds
y <= max LY ) ) by XXREAL_2:def 8;
then consider py being Element of BinFinTrees IndexedREAL such that
A8: ( max LY = Vrootl py & py in Y ) by A7;
py in Z by A8, A1, XBOOLE_0:def 3;
then Vrootl py in L by A2;
then A9: max LY <= MaxVl Z by A8, XXREAL_2:def 8, A2;

per cases by XBOOLE_0:def 3, A3, A1;

suppose p in X ; :: thesis:

then Vrootl p in LX by A4;
then MaxVl Z <= max LX by XXREAL_2:def 8, A3;
then MaxVl Z = max LX by A6, XXREAL_0:1;
hence MaxVl Z = max ((MaxVl X),(MaxVl Y)) by A4, A7, A9, XXREAL_0:def 10; :: thesis:

end;

suppose p in Y ; :: thesis:

then Vrootl p in LY by A7;
then MaxVl Z <= max LY by XXREAL_2:def 8, A3;
then MaxVl Z = max LY by A9, XXREAL_0:1;
hence MaxVl Z = max ((MaxVl X),(MaxVl Y)) by A4, A7, A6, XXREAL_0:def 10; :: thesis:

end;

end;