let S be non empty non void strict ManySortedSign ; :: thesis: for A being strict non-empty MSAlgebra of S holds A = A Over S
let A be strict non-empty MSAlgebra of S; :: thesis: A = A Over S
A1: the carrier of S = dom the Sorts of A by PARTFUN1:def 2;
A2: the carrier' of S = dom the Charact of A by PARTFUN1:def 2;
A3: the Charact of (A Over S) = the Charact of A | the carrier' of S by Def2
.= the Charact of A by A2, RELAT_1:68 ;
the Sorts of (A Over S) = the Sorts of A | the carrier of S by Def2
.= the Sorts of A by A1, RELAT_1:68 ;
hence A = A Over S by A3; :: thesis: verum