theorem Th32: :: ABCMIZ_A:32

for S being non empty non void ManySortedSign
for Y being empty-yielding ManySortedSet of the carrier of S
for X, o being set
for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (S,Y)) & o -tree p in X holds
p is FinSequence of X