let a be object ; :: thesis:
let S be non empty non void ManySortedSign ; :: thesis:
let s be SortSymbol of S; :: thesis:
let X be V5() ManySortedSet of the carrier of S; :: thesis:
let x be Element of X . s; :: thesis:
let t be Element of (Free (S,X)); :: thesis:
assume Z0: t . a = [x,s] ; :: thesis:
then reconsider q = a as Element of dom t by FUNCT_1:def 2;
reconsider v = t | q as Element of (Free (S,X)) by MSAFREE4:44;
{} in (dom t) | q by TREES_1:22;
then A2: v . {} = t . (q ^ (<*> NAT)) by TREES_2:def 10;

per cases by Th16;

suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st v = o -term p ; :: thesis:

then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A1: v = o -term p ;
( [o, the carrier of S] = v . {} & v . {} = [x,s] ) by Z0, A1, A2, TREES_4:def 4;
then ( s in the carrier of S & the carrier of S = s ) by XTUPLE_0:1;
hence a in Leaves (dom t) ; :: thesis:

end;

suppose ex s1 being SortSymbol of S ex x11 being Element of X . s1 st v = x11 -term ; :: thesis:

then consider s1 being SortSymbol of S, x11 being Element of X . s1 such that
A1: v = x11 -term ;
reconsider r = <*0*> as FinSequence of NAT ;

now :: thesis:

assume q ^ <*0*> in dom t ; :: thesis:
then ( r in (dom t) | q & (dom t) | q = dom v ) by TREES_1:def 6, TREES_2:def 10;
then <*0*> in {{}} by A1, TREES_1:29;
hence contradiction ; :: thesis:

end;

hence a in Leaves (dom t) by TREES_1:54; :: thesis:

end;

end;