let S be non void Signature; :: thesis: for X, Y being non-empty 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 non-empty 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 S₁[ 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
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
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 = (the_arity_of o) . 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 = (the_arity_of o) . i ) )
assume A5: i in dom p ; :: thesis: ex t9 being Term of S,X st
( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )
then reconsider t = p . i as Term of S,Y by MSATERM:22;
A6: t in rng p by A5, FUNCT_1:def 3;
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 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 object ; :: 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 A7: x in (Y variables_in ([o, the carrier of S] -tree p)) . s by A6, Th13;
(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 = (the_arity_of o) . i )
thus t9 = p . i ; :: thesis: the_sort_of t9 = (the_arity_of o) . i
the_sort_of t = (the_arity_of o) . i by A5, MSATERM:23;
hence the_sort_of t9 = (the_arity_of o) . i by Th29; :: thesis: verum

end;

len p = len (the_arity_of o) by MSATERM:22;
then reconsider p = p as ArgumentSeq of Sym (o,X) by A4, 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 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 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 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 A10, ZFMISC_1:31;
hence root-tree [x,s] is Term of S,X by MSATERM:4; :: thesis: verum

end;

for t being Term of S,Y holds S₁[t] from MSATERM:sch 1(A9, A1);
hence t is Term of S,X by A8; :: thesis: verum