let S1, S2 be non empty Signature; :: thesis: for A being MSAlgebra over S1 st A is MSAlgebra over S2 holds
( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )
let A be MSAlgebra over S1; :: thesis: ( A is MSAlgebra over S2 implies ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 ) )
assume A is MSAlgebra over S2 ; :: thesis: ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )
then reconsider B = A as MSAlgebra over S2 ;
the Sorts of A = the Sorts of B ;
then dom the Sorts of A = the carrier of S2 by PARTFUN1:def 2;
hence the carrier of S1 = the carrier of S2 by PARTFUN1:def 2; :: thesis: the carrier' of S1 = the carrier' of S2
the Charact of A = the Charact of B ;
then dom the Charact of A = the carrier' of S2 by PARTFUN1:def 2;
hence the carrier' of S1 = the carrier' of S2 by PARTFUN1:def 2; :: thesis: verum