for I, J being set
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 J = [o, the carrier of S] holds
(o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )