consider U1 being non-empty OSAlgebra of non-empty ;
reconsider X = the Sorts of U1 as V5() ManySortedSet of ;
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