:: deftheorem Def17 defines MSCng MSUALG_4:def 17 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for s being SortSymbol of S
for b₆ being Equivalence_Relation of ( the Sorts of U1 . s) holds
( b₆ = MSCng (F,s) iff for x, y being Element of the Sorts of U1 . s holds
( [x,y] in b₆ iff (F . s) . x = (F . s) . y ) );