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 s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))