theorem Th130: :: ABCMIZ_1:130

for S being non void Signature
for X being non empty ManySortedSet of the carrier of S
for f being term-transformation of S,X
for s being SortSymbol of S
for p being FinSequence of the Sorts of (Free (S,X)) . s holds
( f * p is FinSequence of the Sorts of (Free (S,X)) . s & card (f * p) = len p )