A1: ( dom (doms p) = dom p & rng p c= FinTrees D ) by FINSEQ_1:def 4, TREES_3:39;
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 rng (doms p) or x in FinTrees )
assume x in rng (doms p) ; :: thesis: x in FinTrees
then consider y being set such that
A2: ( y in dom p & x = (doms p) . y ) by A1, FUNCT_1:def 5;
reconsider T = p . y as DecoratedTree by A2, TREES_3:26;
T in rng p by A2, FUNCT_1:def 5;
then T is Element of FinTrees D by A1;
then dom T is finite ;
then dom T in FinTrees by TREES_3:def 2;
hence x in FinTrees by A2, FUNCT_6:31; :: thesis: verum

end;