set U1 = the non-empty OSAlgebra of S;
reconsider X = the Sorts of the non-empty OSAlgebra of S as V2() ManySortedSet of S ;
take FreeOSA X ; :: thesis: ( FreeOSA X is osfree & FreeOSA X is strict )
thus ( FreeOSA X is osfree & FreeOSA X is strict ) by Th39; :: thesis: verum