for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S
for t being Element of A2
for p being Element of dom t holds t | p is Element of A2