consider U1 being non-empty OSAlgebra of S;
reconsider X = the Sorts of U1 as V16() 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 Th40; :: thesis: verum