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