let n, m be Element of NAT ; :: thesis: <*0 *> in dom ((elementary_tree 1) --> [n,m])
<*0 *> in elementary_tree 1 by TARSKI:def 2, TREES_1:88;
hence <*0 *> in dom ((elementary_tree 1) --> [n,m]) by FUNCOP_1:19; :: thesis: verum