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 A3: x in rng (doms p) ; :: thesis: x in FinTrees
consider y being set such that
A4: y in dom p and
A5: x = (doms p) . y by A1, A3, FUNCT_1:def 5;
reconsider T = p . y as DecoratedTree by A4, TREES_3:26;
A6: T in rng p by A4, FUNCT_1:def 5;
A7: dom T in FinTrees by A2, A6, TREES_3:def 2;
thus x in FinTrees by A4, A5, A7, FUNCT_6:31; :: thesis: verum

end;