theorem Th20: :: MSATERM:20

for S being non empty non void ManySortedSign
for V being non-empty 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