theorem :: TREES_4:14

for x being object
for T1, T2 being DecoratedTree holds dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2))