let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being compound Element of (Free (S,X)) holds t = (main-constr t) -term (args t)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being compound Element of (Free (S,X)) holds t = (main-constr t) -term (args t)
let t be compound Element of (Free (S,X)); :: thesis: t = (main-constr t) -term (args t)
consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A1: t = o -term p by Th17;
( [o, the carrier of S] -tree p = t & t = (t . {}) -tree (args t) ) by A1, ABCMIZ_A:def 10;
then ( args t = p & [o, the carrier of S] `1 = (t . {}) `1 & (t . {}) `1 = main-constr t ) by TREES_4:15, ABCMIZ_A:def 9;
hence t = (main-constr t) -term (args t) by A1; :: thesis: verum