let x be set ; :: thesis: for T1, T2 being DecoratedTree holds dom (x -tree T1,T2) = tree (dom T1),(dom T2)
let T1, T2 be DecoratedTree; :: thesis: dom (x -tree T1,T2) = tree (dom T1),(dom T2)
( dom (x -tree <*T1,T2*>) = tree (doms <*T1,T2*>) & doms <*T1,T2*> = <*(dom T1),(dom T2)*> ) by Th10, FUNCT_6:34;
hence dom (x -tree T1,T2) = tree (dom T1),(dom T2) by TREES_3:def 17; :: thesis: verum