for S being non empty non void ManySortedSign
for s being SortSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for y being Element of Y . s
for Q being b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b₄ -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
h2 . v is y -omitting