:: deftheorem Def5 defines Normalized MSALIMIT:def 5 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B, b₅ being Binding of OAF holds
( b₅ = Normalized B iff for i, j being Element of P st i >= j holds
b₅ . (j,i) = IFEQ (j,i,(id the Sorts of (OAF . i)),((bind (B,i,j)) ** (id the Sorts of (OAF . i)))) );