:: deftheorem Def3 defines MSAlg_morph MSINST_1:def 3 :
for S being non empty non void ManySortedSign
for A being non empty set
for i, j being set st i in MSAlg_set (S,A) & j in MSAlg_set (S,A) holds
for b₅ being set holds
( b₅ = MSAlg_morph (S,A,i,j) iff for x being set holds
( x in b₅ iff ex M, N being strict feasible MSAlgebra over S ex f being ManySortedFunction of M,N st
( M = i & N = j & f = x & the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N ) ) );