let a be object ; :: thesis: for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let x be Element of X . s; :: thesis: for t being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let t be Element of (Free (S,X)); :: thesis: ( t . a = [x,s] implies a in Leaves (dom t) )
assume Z0: t . a = [x,s] ; :: thesis: a in Leaves (dom t)
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 ( ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st v = o -term p or ex s1 being SortSymbol of S ex x11 being Element of X . s1 st v = x11 -term ) 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: a in Leaves (dom t)

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: verum

end;

suppose ex s1 being SortSymbol of S ex x11 being Element of X . s1 st v = x11 -term ; :: thesis: a in Leaves (dom t)

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: not q ^ <*0*> in dom t

assume q ^ <*0*> in dom t ; :: thesis: contradiction
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: verum

end;

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

end;

end;