let S1, S2 be non empty Signature; :: thesis: for A being MSAlgebra of S1 st A is MSAlgebra of S2 holds
( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )
let A be MSAlgebra of S1; :: thesis: ( A is MSAlgebra of S2 implies ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 ) )
assume A is MSAlgebra of S2 ; :: thesis: ( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )
then reconsider B = A as MSAlgebra of S2 ;
the Sorts of A = the Sorts of B ;
then dom the Sorts of A = the carrier of S2 by PARTFUN1:def 4;
hence the carrier of S1 = the carrier of S2 by PARTFUN1:def 4; :: 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 4;
hence the carrier' of S1 = the carrier' of S2 by PARTFUN1:def 4; :: thesis: verum