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;

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

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

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 that 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;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

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

the_sort_of t = s
by A8, MSATERM:14;
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;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

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