let S be non empty strict ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
let A be non-empty MSAlgebra over S; :: thesis: A +* A = MSAlgebra(# the Sorts of A, the Charact of A #)
set A9 = MSAlgebra(# the Sorts of A, the Charact of A #);
set SA = the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #);
set CA = the Charact of MSAlgebra(# the Sorts of A, the Charact of A #);
set SAA = the Sorts of (A +* A);
set CAA = the Charact of (A +* A);
the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) = the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) +* the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) ;
then A1: the Charact of (A +* A) = the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) by Def4;
the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) = the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) +* the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) ;
then the Sorts of (A +* A) = the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) by Def4;
hence A +* A = MSAlgebra(# the Sorts of A, the Charact of A #) by A1; :: thesis: verum