let n, m be Nat; :: thesis: <*0*> in dom ((elementary_tree 1) --> [n,m])
<*0*> in elementary_tree 1 by TARSKI:def 2, TREES_1:51;
hence <*0*> in dom ((elementary_tree 1) --> [n,m]) by FUNCOP_1:13; :: thesis: verum