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:56;
hence T = root-tree (T . {} ) by A1, FUNCOP_1:17; :: thesis: verum