for i being Nat
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for T being b₄,b₂ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for q being Element of Args (o,T) st i in dom q holds
the_sort_of (q /. i) = (the_arity_of o) /. i