A1: dom (doms p) = dom p by TREES_3:39;
A2: rng p c= FinTrees D by FINSEQ_1:def 4;
thus doms p is FinSequence of FinTrees :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3,FINSEQ_1:def 4 :: thesis: ( not x in proj2 (doms p) or x in FinTrees )
assume x in rng (doms p) ; :: thesis: x in FinTrees
then consider y being set such that
A4: y in dom p and
A5: x = (doms p) . y by A1, FUNCT_1:def 5;
reconsider T = p . y as DecoratedTree by A4, TREES_3:26;
T in rng p by A4, FUNCT_1:def 5;
then dom T in FinTrees by A2, TREES_3:def 2;
hence x in FinTrees by A4, A5, FUNCT_6:31; :: thesis: verum

end;