set D = the Charact of A | the carrier' of S;
set C = the Sorts of A | the carrier of S;
A2: rng the Arity of S c= the carrier of S * ;
A3: the carrier' of S c= the carrier' of S9 by A1, Def1;
then reconsider D = the Charact of A | the carrier' of S as ManySortedSet of the carrier' of S ;
A4: the carrier of S c= the carrier of S9 by A1, Def1;
then reconsider C = the Sorts of A | the carrier of S as ManySortedSet of the carrier of S ;
rng the ResultSort of S c= the carrier of S ;
then A5: C * the ResultSort of S = the Sorts of A * the ResultSort of S by Th1
.= the Sorts of A * (the ResultSort of S9 | the carrier' of S) by A1, Def1
.= (the Sorts of A * the ResultSort of S9) | the carrier' of S by RELAT_1:112 ;
(C # ) * the Arity of S = ((the Sorts of A # ) | (the carrier of S * )) * the Arity of S by A4, Th4
.= (the Sorts of A # ) * the Arity of S by A2, Th1
.= (the Sorts of A # ) * (the Arity of S9 | the carrier' of S) by A1, Def1
.= ((the Sorts of A # ) * the Arity of S9) | the carrier' of S by RELAT_1:112 ;
then reconsider D = D as ManySortedFunction of (C # ) * the Arity of S,C * the ResultSort of S by A3, A5, Th8;
reconsider B = MSAlgebra(# C,D #) as strict non-empty MSAlgebra of S by MSUALG_1:def 8;
take B ; :: thesis: ( the Sorts of B = the Sorts of A | the carrier of S & the Charact of B = the Charact of A | the carrier' of S )
thus ( the Sorts of B = the Sorts of A | the carrier of S & the Charact of B = the Charact of A | the carrier' of S ) ; :: thesis: verum