let S be non empty non void ManySortedSign ; :: thesis: 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
let V be non-empty ManySortedSet of the carrier of S; :: thesis: 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
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o
let p be ArgumentSeq of Sym (o,V); :: thesis: the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o
A1: ([o, the carrier of S] -tree p) . {} = [o, the carrier of S] by TREES_4:def 4;
[o, the carrier of S] = Sym (o,V) by MSAFREE:def 9;
hence the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o by A1, Th17; :: thesis: verum