let S be locally_directed OrderSortedSign; :: thesis: for X being V2() ManySortedSet of S holds FreeOSA X is osfree
let X be V2() 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 Th38; :: thesis: verum