let D be non empty set ; :: thesis: for p being FinSequence of FinTrees D holds p is FinSequence of Trees D
FinTrees D is non empty Subset of (Trees D) by TREES_3:22;
hence for p being FinSequence of FinTrees D holds p is FinSequence of Trees D by FINSEQ_2:27; :: thesis: verum