:: deftheorem Def10 defines canonical_homomorphism MSAFREE4:def 10 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b₂,b₁ -terms all_vars_including MSAlgebra over S
for b₄ being ManySortedFunction of (Free (S,X)),A1 holds
( b₄ = canonical_homomorphism A1 iff ( b₄ is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b₄ || G ) ) );