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;
dom the Charact of A = the carrier' of S by PARTFUN1:def 4;
then A1: 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;
dom the Sorts of A = the carrier of S by PARTFUN1:def 4;
then A2: the Sorts of MSAlgebra(# the Sorts of A,the Charact of A #) = the Sorts of A * (id the carrier of S) by RELAT_1:78;
id the carrier of S, id the carrier' of S form_morphism_between S,S by Th9;
hence A | S,(id the carrier of S),(id the carrier' of S) = MSAlgebra(# the Sorts of A,the Charact of A #) by A2, A1, Def3; :: thesis: verum