let x be set ; :: thesis: for S being non void Signature
for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let S be non void Signature; :: thesis: for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let Y be non-empty ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S holds
( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
let s be SortSymbol of S; :: thesis: ( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )
A1: (S -Terms (X,Y)) . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by Def5;

hereby :: thesis: ( x in X . s & x in Y . s implies root-tree [x,s] in (S -Terms (X,Y)) . s )

assume root-tree [x,s] in (S -Terms (X,Y)) . s ; :: thesis: ( x in X . s & x in Y . s )
then consider t being Term of S,Y such that
A2: root-tree [x,s] = t and
the_sort_of t = s and
A3: variables_in t c= X by A1;
A4: t . {} = [x,s] by A2, TREES_4:3;
s in the carrier of S ;
then s <> the carrier of S ;
then not s in { the carrier of S} by TARSKI:def 1;
then not t . {} in [: the carrier' of S,{ the carrier of S}:] by A4, ZFMISC_1:87;
then consider s9 being SortSymbol of S, v being Element of Y . s9 such that
A5: t . {} = [v,s9] by MSATERM:2;
A6: ( s = s9 & x = v ) by A4, A5, XTUPLE_0:1;
( (S variables_in t) . s = {x} & (variables_in t) . s c= X . s ) by A2, A3, Th10;
hence ( x in X . s & x in Y . s ) by A6, ZFMISC_1:31; :: thesis: verum

end;

assume that
A7: x in X . s and
A8: x in Y . s ; :: thesis: root-tree [x,s] in (S -Terms (X,Y)) . s
reconsider t = root-tree [x,s] as Term of S,Y by A8, MSATERM:4;
A9: variables_in t c= X

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or (variables_in t) . i c= X . i )
assume i in the carrier of S ; :: thesis: (variables_in t) . i c= X . i
A10: (S variables_in t) . s = {x} by Th10;
( i <> s implies (S variables_in t) . i = {} ) by Th10;
hence (variables_in t) . i c= X . i by A7, A10, ZFMISC_1:31; :: thesis: verum

end;

the_sort_of t = s by A8, MSATERM:14;
hence root-tree [x,s] in (S -Terms (X,Y)) . s by A1, A9; :: thesis: verum