let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S holds FreeMSA X is free
let X be non-empty ManySortedSet of the carrier of S; :: thesis: FreeMSA X is free
take FreeGen X ; :: according to MSAFREE:def 6 :: thesis: FreeGen X is free
thus FreeGen X is free by Th16; :: thesis: verum