A1: ( Free (S,X) = FreeMSA X & FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) ) by MSAFREE3:31;
then A2: p is ArgumentSeq of Sym (o,X) by INSTALG1:1;
then reconsider t = (Sym (o,X)) -tree p as Term of S,X by MSATERM:1;
the_sort_of t = the_result_sort_of o by A2, MSATERM:20;
then t in FreeSort (X,(the_result_sort_of o)) by MSATERM:def 5;
hence [o, the carrier of S] -tree p is Element of (Free (S,X)),(the_result_sort_of o) by A1, MSAFREE:def 11; :: thesis: verum