let x be set ; :: thesis: ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x )
( root-tree x = (elementary_tree 0 ) --> x & {} in elementary_tree 0 ) by TARSKI:def 1, TREES_1:56;
hence ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x ) by FUNCOP_1:13, FUNCOP_1:19; :: thesis: verum