let S be non empty non void ManySortedSign ; :: thesis: for V being V16() 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 V16() 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 11;
hence the_sort_of ((Sym o,V) -tree p) = the_result_sort_of o by A1, Th17; :: thesis: verum