let x be set ; :: thesis: for S being non void Signature
for Y being V5 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 V5 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 V5 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 Def6;

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 & the_sort_of t = s & variables_in t c= X ) by A1;
s in the carrier of S ;
then s <> the carrier of S ;
then A3: ( t . {} = [x,s] & not s in {the carrier of S} ) by A2, TARSKI:def 1, TREES_4:3;
then not t . {} in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:106;
then consider s' being SortSymbol of S, v being Element of Y . s' such that
A4: t . {} = [v,s'] by MSATERM:2;
A5: ( s = s' & x = v ) by A3, A4, ZFMISC_1:33;
( variables_in t = S variables_in t & (S variables_in t) . s = {x} & (variables_in t) . s c= X . s ) by A2, Th11, PBOOLE:def 5;
hence ( x in X . s & x in Y . s ) by A5, ZFMISC_1:37; :: thesis: verum

end;

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

proof

let i be set ; :: according to PBOOLE:def 5 :: 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
( ( i <> s implies (S variables_in t) . i = {} ) & (S variables_in t) . s = {x} ) by Th11;
hence (variables_in t) . i c= X . i by A6, XBOOLE_1:2, ZFMISC_1:37; :: thesis: verum

end;

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