let S be non void Signature; :: thesis: for X, Y being V5() ManySortedSet of
for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X
let X, Y be V5() ManySortedSet of ; :: thesis: for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X
defpred S₁[ DecoratedTree] means ( Y variables_in $1 c= X implies $1 is Term of S,X );
A1: for s being SortSymbol of S
for x being Element of Y . s holds S₁[ root-tree [x,s]]

proof

let s be SortSymbol of S; :: thesis: for x being Element of Y . s holds S₁[ root-tree [x,s]]
let x be Element of Y . s; :: thesis: S₁[ root-tree [x,s]]
assume Y variables_in (root-tree [x,s]) c= X ; :: thesis: root-tree [x,s] is Term of S,X
then ( (Y variables_in (root-tree [x,s])) . s = {x} & (Y variables_in (root-tree [x,s])) . s c= X . s ) by Th13, PBOOLE:def 5;
then x in X . s by ZFMISC_1:37;
hence root-tree [x,s] is Term of S,X by MSATERM:4; :: thesis: verum

end;

A2: for o being OperSymbol of S
for p being ArgumentSeq of Sym o,Y st ( for t being Term of S,Y st t in rng p holds
S₁[t] ) holds
S₁[[o,the carrier of S] -tree p]

proof

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym o,Y st ( for t being Term of S,Y st t in rng p holds
S₁[t] ) holds
S₁[[o,the carrier of S] -tree p]
let p be ArgumentSeq of Sym o,Y; :: thesis: ( ( for t being Term of S,Y st t in rng p holds
S₁[t] ) implies S₁[[o,the carrier of S] -tree p] )
assume that
A3: for t being Term of S,Y st t in rng p & Y variables_in t c= X holds
t is Term of S,X and
A4: Y variables_in ([o,the carrier of S] -tree p) c= X ; :: thesis: [o,the carrier of S] -tree p is Term of S,X
A5: len p = len (the_arity_of o) by MSATERM:22;

now

let i be Nat; :: thesis: ( i in dom p implies ex t' being Term of S,X st
( t' = p . i & the_sort_of t' = (the_arity_of o) . i ) )
assume A6: i in dom p ; :: thesis: ex t' being Term of S,X st
( t' = p . i & the_sort_of t' = (the_arity_of o) . i )
then reconsider t = p . i as Term of S,Y by MSATERM:22;
A7: ( the_sort_of t = (the_arity_of o) . i & t in rng p ) by A6, FUNCT_1:def 5, MSATERM:23;
Y variables_in t c= X

proof

let y be set ; :: according to PBOOLE:def 5 :: thesis: ( not y in the carrier of S or (Y variables_in t) . y c= X . y )
assume y in the carrier of S ; :: thesis: (Y variables_in t) . y c= X . y
then reconsider s = y as SortSymbol of S ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (Y variables_in t) . y or x in X . y )
assume x in (Y variables_in t) . y ; :: thesis: x in X . y
then ( (Y variables_in ([o,the carrier of S] -tree p)) . s c= X . s & x in (Y variables_in ([o,the carrier of S] -tree p)) . s ) by A4, A7, Th14, PBOOLE:def 5;
hence x in X . y ; :: thesis: verum

end;

then reconsider t' = t as Term of S,X by A3, A7;
take t' = t'; :: thesis: ( t' = p . i & the_sort_of t' = (the_arity_of o) . i )
thus t' = p . i ; :: thesis: the_sort_of t' = (the_arity_of o) . i
thus the_sort_of t' = (the_arity_of o) . i by A7, Th30; :: thesis: verum

end;

then reconsider p = p as ArgumentSeq of Sym o,X by A5, MSATERM:24;
(Sym o,X) -tree p is Term of S,X ;
hence [o,the carrier of S] -tree p is Term of S,X by MSAFREE:def 11; :: thesis: verum

end;

let t be Term of S,Y; :: thesis: ( variables_in t c= X implies t is Term of S,X )
assume variables_in t c= X ; :: thesis: t is Term of S,X
then A8: Y variables_in t c= X by Th16;
for t being Term of S,Y holds S₁[t] from MSATERM:sch 1(A1, A2);
hence t is Term of S,X by A8; :: thesis: verum