let S be non void Signature; :: thesis: for X, Y being V8() ManySortedSet of the carrier of S
for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X

let X, Y be V8() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,Y st variables_in t c= X holds
t is Term of S,X

defpred S1[ DecoratedTree] means ( Y variables_in \$1 c= X implies \$1 is Term of S,X );
let t be Term of S,Y; :: thesis: ( variables_in t c= X implies t is Term of S,X )
A1: 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
S1[t] ) holds
S1[[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
S1[t] ) holds
S1[[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
S1[t] ) implies S1[[o, the carrier of S] -tree p] )

assume that
A2: 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
A3: 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
A4: now :: thesis: for i being Nat st i in dom p holds
ex t9 being Term of S,X st
( t9 = p . i & the_sort_of t9 = () . i )
let i be Nat; :: thesis: ( i in dom p implies ex t9 being Term of S,X st
( t9 = p . i & the_sort_of t9 = () . i ) )

assume A5: i in dom p ; :: thesis: ex t9 being Term of S,X st
( t9 = p . i & the_sort_of t9 = () . i )

then reconsider t = p . i as Term of S,Y by MSATERM:22;
A6: t in rng p by ;
Y variables_in t c= X
proof
let y be object ; :: according to PBOOLE:def 2 :: thesis: ( not y in the carrier of S or () . y c= X . y )
assume y in the carrier of S ; :: thesis: () . y c= X . y
then reconsider s = y as SortSymbol of S ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () . y or x in X . y )
assume x in () . y ; :: thesis: x in X . y
then A7: x in (Y variables_in ([o, the carrier of S] -tree p)) . s by ;
(Y variables_in ([o, the carrier of S] -tree p)) . s c= X . s by A3;
hence x in X . y by A7; :: thesis: verum
end;
then reconsider t9 = t as Term of S,X by A2, A6;
take t9 = t9; :: thesis: ( t9 = p . i & the_sort_of t9 = () . i )
thus t9 = p . i ; :: thesis: the_sort_of t9 = () . i
the_sort_of t = () . i by ;
hence the_sort_of t9 = () . i by Th29; :: thesis: verum
end;
len p = len () by MSATERM:22;
then reconsider p = p as ArgumentSeq of Sym (o,X) by ;
(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 9; :: thesis: verum
end;
assume variables_in t c= X ; :: thesis: t is Term of S,X
then A8: Y variables_in t c= X by Th15;
A9: for s being SortSymbol of S
for x being Element of Y . s holds S1[ root-tree [x,s]]
proof
let s be SortSymbol of S; :: thesis: for x being Element of Y . s holds S1[ root-tree [x,s]]
let x be Element of Y . s; :: thesis: S1[ 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 A10: (Y variables_in (root-tree [x,s])) . s c= X . s ;
(Y variables_in (root-tree [x,s])) . s = {x} by Th12;
then x in X . s by ;
hence root-tree [x,s] is Term of S,X by MSATERM:4; :: thesis: verum
end;
for t being Term of S,Y holds S1[t] from hence t is Term of S,X by A8; :: thesis: verum