ManySortedSign(# the carrier of (S1 +* S2), the carrier' of (S1 +* S2), the Arity of (S1 +* S2), the ResultSort of (S1 +* S2) #) = S1 +* S2 by Def52;
then reconsider A = A1 +* A2 as MSAlgebra over S1 +* S2 ;
A is non-empty ;
then reconsider A = A1 +* A2 as non-empty MSAlgebra over S1 +* S2 ;
A = MSAlgebra(# the Sorts of A, the Charact of A #) ;
hence A1 +* A2 is strict non-empty MSAlgebra over S1 +* S2 ; :: thesis: verum