set x = A | a;
A1: dom (A | a) = (dom A) | a by TREES_2:def 11;
then reconsider db = dom (A | a) as finite Tree ;
reconsider x = A | a as finite DecoratedTree of by A1, Lm2;

now

set da = dom A;
thus db is finite ; :: thesis: for v being Element of db 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 ] ) )
let v be Element of db; :: 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 ] ) )
v in db ;
then A2: v in (dom A) | a by TREES_2:def 11;
then reconsider w = a ^ v as Element of dom A by TREES_1:def 9;
reconsider v' = v as Element of (dom A) | a by TREES_2:def 11;
X: succ v', succ w are_equipotent by Th20;
succ v' = succ v by TREES_2:def 11;
then card (succ v) = card (succ w) by X, CARD_1:21;
then branchdeg v = card (succ w) by TREES_2:def 13;
then A3: branchdeg v = branchdeg w by TREES_2:def 13;
hence branchdeg v <= 2 by Def6; :: 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] ) :: thesis: ( ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) )

proof

assume A4: branchdeg v = 0 ; :: thesis: ( x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] )

per cases ( A . w = [0 ,0 ] or ex k being Element of NAT st A . w = [3,k] ) by A3, A4, Def6;

suppose A . w = [0 ,0 ] ; :: thesis: ( x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] )

hence ( x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) by A2, TREES_2:def 11; :: thesis: verum

end;

suppose ex k being Element of NAT st A . w = [3,k] ; :: thesis: ( x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] )

then consider k being Element of NAT such that
A5: A . w = [3,k] ;

now

take k = k; :: thesis: x . v = [3,k]
thus x . v = [3,k] by A2, A5, TREES_2:def 11; :: thesis: verum

end;

hence ( x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) ; :: thesis: verum

end;

end;

end;

thus ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) :: thesis: ( branchdeg v = 2 implies x . v = [2,0 ] )

proof

assume A6: branchdeg v = 1 ; :: thesis: ( x . v = [1,0 ] or x . v = [1,1] )

per cases ( A . w = [1,0 ] or A . w = [1,1] ) by A3, A6, Def6;

suppose A . w = [1,0 ] ; :: thesis: ( x . v = [1,0 ] or x . v = [1,1] )

hence ( x . v = [1,0 ] or x . v = [1,1] ) by A2, TREES_2:def 11; :: thesis: verum

end;

suppose A . w = [1,1] ; :: thesis: ( x . v = [1,0 ] or x . v = [1,1] )

hence ( x . v = [1,0 ] or x . v = [1,1] ) by A2, TREES_2:def 11; :: thesis: verum

end;

end;

end;

thus ( branchdeg v = 2 implies x . v = [2,0 ] ) :: thesis: verum

proof

assume branchdeg v = 2 ; :: thesis: x . v = [2,0 ]
then A . w = [2,0 ] by A3, Def6;
hence x . v = [2,0 ] by A2, TREES_2:def 11; :: thesis: verum

end;

end;

hence A | a is MP-wff by Def6; :: thesis: verum