for S being non empty non void ManySortedSign
for o being OperSymbol of S
for V being V2() ManySortedSet of the carrier of S
for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x