let x be set ; 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; 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; 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; 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; ( 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 ( 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
;
( 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;
verum
end;
assume that
A7:
x in X . s
and
A8:
x in Y . s
; 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
the_sort_of t = s
by A8, MSATERM:14;
hence
root-tree [x,s] in (S -Terms (X,Y)) . s
by A1, A9; verum