let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S holds FreeMSA X is free

let X be V5() 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

let X be V5() 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