let S be 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
let V be 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
let o be 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 p be ArgumentSeq of Sym (o,V); 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; verum