let S be non empty non void strict ManySortedSign ; :: thesis: for A being strict non-empty MSAlgebra over S holds A = A Over S
let A be strict non-empty MSAlgebra over S; :: thesis: A = A Over S
A1: the Charact of (A Over S) = the Charact of A | the carrier' of S by Def2
.= the Charact of A ;
the Sorts of (A Over S) = the Sorts of A | the carrier of S by Def2
.= the Sorts of A ;
hence A = A Over S by A1; :: thesis: verum