theorem :: MSAFREE:14

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S holds FreeGen X is V5()