:: deftheorem HOM defines Hom MSAFREE5:def 31 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for s being SortSymbol of S
for x1, x2 being Element of X . s
for b₇ being Endomorphism of T holds
( b₇ = Hom (T,x1,x2) iff ( (b₇ . s) . (x1 -term) = x2 -term & (b₇ . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(b₇ . s1) . (y -term) = y -term ) ) );