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 . {} )
A2: for x being set st x in dom T holds
T . x = T . {} by A1, TARSKI:def 1, TREES_1:56;
thus T = root-tree (T . {} ) by A1, A2, FUNCOP_1:17; :: thesis: verum