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