for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))