:: deftheorem Def20 defines NFAlgebra MSAFREE4:def 20 :
for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for b₄ being strict non-empty MSAlgebra over S holds
( b₄ = NFAlgebra R iff ( the Sorts of b₄ = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b₄) holds (Den (o,b₄)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) ) );