for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b₂,b₁ -terms all_vars_including MSAlgebra over S
for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))