:: deftheorem Def2 defines Binding MSALIMIT:def 2 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for b₄ being ManySortedFunction of the InternalRel of P holds
( b₄ is Binding of OAF iff for i, j, k being Element of P st i >= j & j >= k holds
ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = b₄ . (j,i) & f2 = b₄ . (k,j) & b₄ . (k,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) );