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