theorem Th90: :: MSAFREE5:112

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for t being Element of (Free (S,X)) holds R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t