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