theorem Th8: :: MSAFREE:8

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)