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 object st x in dom T holds

T . x = T . {} by TARSKI:def 1, TREES_1:29;

hence T = root-tree (T . {}) by A1; :: thesis: verum

assume A1: dom T = elementary_tree 0 ; :: thesis: T = root-tree (T . {})

then for x being object st x in dom T holds

T . x = T . {} by TARSKI:def 1, TREES_1:29;

hence T = root-tree (T . {}) by A1; :: thesis: verum