for P being non empty Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for NB being normalized Binding of OAF
for i, j being Element of P st i >= j holds
(Normalized NB) . (j,i) = NB . (j,i)