for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o