let x be set ; :: thesis: for S being non void Signature
for Y being V8() 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 V8() 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 V8() 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 ;
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 ;
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 ;
( (S variables_in t) . s = {x} & () . s c= X . s ) by A2, A3, Th10;
hence ( x in X . s & x in Y . s ) by ; :: 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 ;
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 () . i c= X . i )
assume i in the carrier of S ; :: thesis: () . i c= X . i
A10: (S variables_in t) . s = {x} by Th10;
( i <> s implies () . i = {} ) by Th10;
hence (variables_in t) . i c= X . i by ; :: thesis: verum
end;
the_sort_of t = s by ;
hence root-tree [x,s] in (S -Terms (X,Y)) . s by A1, A9; :: thesis: verum