theorem Th112: :: MSAFREE5:110

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) holds
( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )