let S be non empty ManySortedSign ; :: thesis: for A being MSAlgebra of S holds A | S,(id the carrier of S),(id the carrier' of S) = MSAlgebra(# the Sorts of A,the Charact of A #)
let A be MSAlgebra of S; :: thesis: A | S,(id the carrier of S),(id the carrier' of S) = MSAlgebra(# the Sorts of A,the Charact of A #)
set f = id the carrier of S;
set g = id the carrier' of S;
A1: id the carrier of S, id the carrier' of S form_morphism_between S,S by Th9;
( dom the Charact of A = the carrier' of S & dom the Sorts of A = the carrier of S ) by PBOOLE:def 3;
then ( the Sorts of MSAlgebra(# the Sorts of A,the Charact of A #) = the Sorts of A * (id the carrier of S) & the Charact of MSAlgebra(# the Sorts of A,the Charact of A #) = the Charact of A * (id the carrier' of S) ) by RELAT_1:78;
hence A | S,(id the carrier of S),(id the carrier' of S) = MSAlgebra(# the Sorts of A,the Charact of A #) by A1, Def3; :: thesis: verum