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

now :: thesis: ( db is finite & ( for v being Element of db holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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 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 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 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] ) )
set da = dom A;
reconsider v9 = v as Element of (dom A) | a by TREES_2:def 10;
v in db ;
then A2: v in (dom A) | a by TREES_2:def 10;
then reconsider w = a ^ v as Element of dom A by TREES_1:def 6;
( succ v9, succ w are_equipotent & succ v9 = succ v ) by Th11, TREES_2:def 10;
then card (succ v) = card (succ w) by CARD_1:5;
then branchdeg v = card (succ w) by TREES_2:def 12;
then A3: branchdeg v = branchdeg w by TREES_2:def 12;
hence branchdeg v <= 2 by Def5; :: thesis: ( ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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 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 Nat st x . v = [3,k] )

per cases ( A . w = [0,0] or ex k being Nat st A . w = [3,k] ) by A3, A4, Def5;

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

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

end;

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

then consider k being Nat such that
A5: A . w = [3,k] ;
x . v = [3,k] by A2, A5, TREES_2:def 10;
hence ( x . v = [0,0] or ex k being 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, Def5;

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 10; :: 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 10; :: 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, Def5;
hence x . v = [2,0] by A2, TREES_2:def 10; :: thesis: verum

end;

end;

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