let x be object ; :: thesis: for T being DecoratedTree holds dom (x -tree T) = ^ (dom T)
let T be DecoratedTree; :: thesis: dom (x -tree T) = ^ (dom T)
( dom (x -tree <*T*>) = tree (doms <*T*>) & doms <*T*> = <*(dom T)*> ) by Th10, FINSEQ_3:132;
hence dom (x -tree T) = ^ (dom T) by TREES_3:def 16; :: thesis: verum