A1: k in NAT by ORDINAL1:def 12;
(Vrootr p) + (Vrootr q) in REAL by XREAL_0:def 1;
then [k,((Vrootr p) + (Vrootr q))] in [:NAT,REAL:] by A1, ZFMISC_1:87;
hence [k,((Vrootr p) + (Vrootr q))] -tree (p,q) is finite binary DecoratedTree of IndexedREAL ; :: thesis: verum