theorem Th78: :: MSAFREE5:100
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st r is x1 -omitting & r is x2 -omitting holds
(Hom (T,x1,x2)) . r = r