:: deftheorem Def18 defines MSCng MSUALG_4:def 18 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
for b₅ being MSCongruence of U1 holds
( b₅ = MSCng F iff for s being SortSymbol of S holds b₅ . s = MSCng (F,s) );