let S be non empty non void ManySortedSign ; :: thesis: for X being V16() ManySortedSet of the carrier of S holds FreeMSA X is free
let X be V16() 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 Th17; :: thesis: verum