let x be set ; :: thesis: ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = 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