for S being non empty non void ManySortedSign
for X being ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) holds
(Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p