theorem Th2: :: MSALIMIT:2

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 holds
for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds
f is_homomorphism OAF . i,OAF . j