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))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
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))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
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))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
let x be Element of X . s; :: thesis: for t being Element of (Free (S,X))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
let t be Element of (Free (S,X)); :: thesis: for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
let xi be Node of t; :: thesis: ( t . xi = [x,s] implies t | xi = x -term )
assume Z0: t . xi = [x,s] ; :: thesis: t | xi = x -term
reconsider tx = t | xi as Element of (Free (S,X)) by MSAFREE4:44;

per cases ( ex s1 being SortSymbol of S ex x11 being Element of X . s1 st tx = x11 -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st tx = o -term p ) by Th16;

suppose ex s1 being SortSymbol of S ex x11 being Element of X . s1 st tx = x11 -term ; :: thesis: t | xi = x -term

then consider s1 being SortSymbol of S, x11 being Element of X . s1 such that
A1: tx = x11 -term ;
( <*> NAT in dom tx & dom tx = (dom t) | xi ) by TREES_1:22, TREES_2:def 10;
then tx . {} = t . (xi ^ {}) by TREES_2:def 10;
hence t | xi = x -term by Z0, A1, TREES_4:3; :: thesis: verum

end;

suppose ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st tx = o -term p ; :: thesis: t | xi = x -term

then consider o being OperSymbol of S, p being Element of Args (o,(Free (S,X))) such that
A2: tx = o -term p ;
( <*> NAT in dom tx & dom tx = (dom t) | xi ) by TREES_1:22, TREES_2:def 10;
then tx . {} = t . (xi ^ {}) by TREES_2:def 10;
then [o, the carrier of S] = [x,s] by Z0, A2, TREES_4:def 4;
then ( s in the carrier of S & the carrier of S = s ) by XTUPLE_0:1;
hence t | xi = x -term ; :: thesis: verum

end;

end;