:: deftheorem Def4 defines normalized MSALIMIT:def 4 :
for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for IT being Binding of OAF holds
( IT is normalized iff for i being Element of P holds IT . (i,i) = id the Sorts of (OAF . i) );