set x = (elementary_tree 0 ) --> [0 ,0 ];
dom ((elementary_tree 0 ) --> [0 ,0 ]) = {{} } by FUNCOP_1:19, TREES_1:56;
then reconsider x = (elementary_tree 0 ) --> [0 ,0 ] as finite DecoratedTree of by Lm2;
A1: dom x = elementary_tree 0 by FUNCOP_1:19;
A2: dom x = {{} } by FUNCOP_1:19, TREES_1:56;
for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

proof

let v be Element of dom x; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )
A3: succ v = {}

proof

assume A4: not succ v = {} ; :: thesis: contradiction
consider y being Element of succ v;
y in succ v by A4;
then y in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in dom x } by TREES_2:def 5;
then consider m being Element of NAT such that
A5: ( y = v ^ <*m*> & v ^ <*m*> in dom x ) ;
thus contradiction by A2, A5, TARSKI:def 1; :: thesis: verum

end;

hence branchdeg v <= 2 by CARD_1:47, TREES_2:def 13; :: thesis: ( ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )
thus ( ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) by A1, A3, CARD_1:47, FUNCOP_1:13, TREES_2:def 13; :: thesis: verum

end;

hence (elementary_tree 0 ) --> [0 ,0 ] is MP-wff by Def6; :: thesis: verum