set S1 = OSSign S0;
set s0 = the Sorts of M;
set c0 = the Charact of M;
A1: the carrier of S0 = the carrier of (OSSign S0) by Def5;
then reconsider s1 = the Sorts of M as ManySortedSet of (OSSign S0) ;
( the Arity of S0 = the Arity of (OSSign S0) & the ResultSort of (OSSign S0) = the ResultSort of S0 ) by Def5;
then reconsider c1 = the Charact of M as ManySortedFunction of (s1 #) * the Arity of (OSSign S0),s1 * the ResultSort of (OSSign S0) by A1, Def5;
MSAlgebra(# s1,c1 #) is order-sorted ;
hence ex b₁ being strict OSAlgebra of OSSign S0 st
( the Sorts of b₁ = the Sorts of M & the Charact of b₁ = the Charact of M ) ; :: thesis: verum