let T be DecoratedTree; :: thesis: ( dom T = elementary_tree 0 implies T = root-tree (T . {}) )
assume A1: dom T = elementary_tree 0 ; :: thesis: T = root-tree (T . {})
then for x being set st x in dom T holds
T . x = T . {} by TARSKI:def 1, TREES_1:29;
hence T = root-tree (T . {}) by A1, FUNCOP_1:11; :: thesis: verum