theorem Th3: :: MSALIMIT:3

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