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:21;
hence for p being FinSequence of FinTrees D holds p is FinSequence of Trees D by FINSEQ_2:24; :: thesis: verum