let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) holds the_sort_of (o -term p) = the_result_sort_of o
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) holds the_sort_of (o -term p) = the_result_sort_of o
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for p being Element of Args (o,(Free (S,X))) holds the_sort_of (o -term p) = the_result_sort_of o
let p be Element of Args (o,(Free (S,X))); :: thesis: the_sort_of (o -term p) = the_result_sort_of o
reconsider t = o -term p as Term of S,X by MSAFREE4:42;
[o, the carrier of S] = t . {} by TREES_4:def 4;
then the_sort_of t = the_result_sort_of o by MSATERM:17;
hence the_sort_of (o -term p) = the_result_sort_of o by Th5; :: thesis: verum