:: deftheorem Def2 defines Over MSUHOM_1:def 2 :
for S, S9 being non empty non void strict ManySortedSign
for A being strict non-empty MSAlgebra over S9 st S <= S9 holds
for b₄ being strict non-empty MSAlgebra over S holds
( b₄ = A Over S iff ( the Sorts of b₄ = the Sorts of A | the carrier of S & the Charact of b₄ = the Charact of A | the carrier' of S ) );