:: deftheorem Def16 defines FreeGen MSAFREE:def 16 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for b₃ being GeneratorSet of FreeMSA X holds
( b₃ = FreeGen X iff for s being SortSymbol of S holds b₃ . s = FreeGen (s,X) );