theorem Th9: :: MSAFREE:9

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )