let S be non empty ManySortedSign ; :: thesis: for A being MSAlgebra over 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 over 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 2;

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:52;

dom the Sorts of A = the carrier of S by PARTFUN1:def 2;

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:52;

id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8;

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

let A be MSAlgebra over 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 2;

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:52;

dom the Sorts of A = the carrier of S by PARTFUN1:def 2;

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:52;

id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8;

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