let x be object ; :: 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, FINSEQ_3:133;
hence dom (x -tree (T1,T2)) = tree ((dom T1),(dom T2)) by TREES_3:def 17; :: thesis: verum