for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A, B being non-empty b₂,b₁ -terms MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
( ( A is all_vars_including implies B is all_vars_including ) & ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) )