:: deftheorem Def6 defines InvLim MSALIMIT:def 6 :
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 b₅ being strict MSSubAlgebra of product OAF holds
( b₅ = InvLim B iff for s being SortSymbol of S
for f being Element of (SORTS OAF) . s holds
( f in the Sorts of b₅ . s iff for i, j being Element of P st i >= j holds
((bind (B,i,j)) . s) . (f . i) = f . j ) );