reconsider a = a as set by TARSKI:1;
( a in dom p or a nin dom p ) ;

per cases then ( p . a is DecoratedTree or p . a is empty ) by FUNCT_1:def 2, TREES_3:24;

suppose p . a is DecoratedTree ; :: thesis: dom (p . a) is FinSequence-membered

then reconsider t = p . a as DecoratedTree ;
dom t is Tree ;
hence dom (p . a) is FinSequence-membered ; :: thesis: verum

end;

suppose p . a is empty ; :: thesis: dom (p . a) is FinSequence-membered

then reconsider t = p . a as empty set ;
dom t is empty ;
hence dom (p . a) is FinSequence-membered ; :: thesis: verum

end;

end;