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

let s be SortSymbol of S; :: thesis:
let v be Element of X . s; :: thesis:
thus S variables_in (root-tree [v,s]) c= X :: thesis:

end;

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

let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of Sym o,X; :: thesis:
assume A3: for t being Term of S,X st t in rng p holds
S variables_in t c= X ; :: thesis:
set q = [o,the carrier of S] -tree p;
thus S variables_in ([o,the carrier of S] -tree p) c= X :: thesis:

let s' be set ; :: according to PBOOLE:def 5 :: thesis:
assume s' in the carrier of S ; :: thesis:
then reconsider z = s' as SortSymbol of S ;
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (S variables_in ([o,the carrier of S] -tree p)) . s' ; :: thesis:
then consider t being DecoratedTree such that
A4: ( t in rng p & x in (S variables_in t) . z ) by Th12;
consider i being set such that
A5: ( i in dom p & t = p . i ) by A4, FUNCT_1:def 5;
reconsider i = i as Nat by A5;
reconsider t = p . i as Term of S,X by A5, MSATERM:22;
S variables_in t c= X by A3, A4, A5;
then (S variables_in t) . z c= X . z by PBOOLE:def 5;
hence x in X . s' by A4, A5; :: thesis:

end;

for t being Term of S,X holds S₁[t] from MSATERM:sch 1(A1, A2);
hence for t being Term of S,X holds S variables_in t c= X ; :: thesis: