for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for s being SortSymbol of S
for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2