theorem Th10: :: MSAFREE:10

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
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )