let S be locally_directed OrderSortedSign; :: thesis: for X being V5() ManySortedSet of S holds FreeOSA X is osfree
let X be V5() ManySortedSet of S; :: thesis: FreeOSA X is osfree
take OSFreeGen X ; :: according to OSAFREE:def 3 :: thesis: OSFreeGen X is osfree
thus OSFreeGen X is osfree by Th39; :: thesis: verum