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

proof

let x be object ; :: 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 object such that
A3: y in dom p and
A4: x = (doms p) . y by A1, FUNCT_1:def 3;
reconsider T = p . y as DecoratedTree by A3, TREES_3:24;
T in rng p by A3, FUNCT_1:def 3;
then dom T in FinTrees by A2, TREES_3:def 2;
hence x in FinTrees by A3, A4, FUNCT_6:22; :: thesis: verum

end;