theorem :: MSALIMIT:5

for DP being non empty discrete Poset
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of DP,S
for B being normalized Binding of OAF holds InvLim B = product OAF