let S be non empty strict ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S holds A +* A = MSAlgebra(# the Sorts of A,the Charact of A #)
let A be non-empty MSAlgebra of S; :: thesis: A +* A = MSAlgebra(# the Sorts of A,the Charact of A #)
set A' = 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 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 #) & 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 ( A +* A = MSAlgebra(# the Sorts of (A +* A),the Charact of (A +* A) #) & MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of MSAlgebra(# the Sorts of A,the Charact of A #),the Charact of MSAlgebra(# the Sorts of A,the Charact of A #) #) & S = S +* S & the Sorts of (A +* A) = the Sorts of MSAlgebra(# the Sorts of A,the Charact of A #) & the Charact of (A +* A) = the Charact of MSAlgebra(# the Sorts of A,the Charact of A #) ) by Def4, Th8;
hence A +* A = MSAlgebra(# the Sorts of A,the Charact of A #) ; :: thesis: verum