:: deftheorem defines Class MSUALG_4:def 5 :
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S
for R being MSEquivalence-like ManySortedRelation of U1
for i being Element of S
for x being Element of the Sorts of U1 . i holds Class (R,x) = Class ((R . i),x);