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 p being Element of Args (o,(Free (S,X))) st ex f being FinSequence of NAT st
( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) holds
deg (o -term p) = i + 1