for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for t1, t2 being Element of (Free (S,X)) st t2 = (canonical_homomorphism T) . t1 holds
(canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2