let x be object ; :: thesis: ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x )

{} in elementary_tree 0 by TARSKI:def 1, TREES_1:29;

hence ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x ) by FUNCOP_1:7; :: thesis: verum

{} in elementary_tree 0 by TARSKI:def 1, TREES_1:29;

hence ( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x ) by FUNCOP_1:7; :: thesis: verum