theorem :: MSAFREE3:25

for S being non void Signature
for X being ManySortedSet of the carrier of S holds (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X)