:: deftheorem Def5 defines hom INSTALG1:def 5 :
for S1, S2 being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for b₆ being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) holds
( b₆ = hom (f,g,X,S1,S2) iff ( b₆ is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b₆ . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) );