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;
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;
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 RELAT_1:83, A1 ;
(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 S9 | the carrier' of S) by A1, A2, Th1
.= (( the Sorts of A #) * the Arity of S9) | the carrier' of S by RELAT_1:83 ;
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 over S by MSUALG_1:def 3;
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