let S be non void Signature; :: thesis: for X being V5 ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t c= X
let X be V5 ManySortedSet of the carrier of S; :: thesis: for t being Term of S,X holds variables_in t c= X
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]]

proof

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

proof

let y be set ; :: according to PBOOLE:def 5 :: thesis: ( not y in the carrier of S or (S variables_in (root-tree [x,s])) . y c= X . y )
assume y in the carrier of S ; :: thesis: (S variables_in (root-tree [x,s])) . y c= X . y
( (S variables_in (root-tree [x,s])) . s = {x} & ( s = y or s <> y ) & ( y <> s implies (S variables_in (root-tree [x,s])) . y = {} ) ) by Th11;
hence (S variables_in (root-tree [x,s])) . y c= X . y by XBOOLE_1:2; :: thesis: verum

end;

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]

proof

let o be OperSymbol of S; :: thesis: 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 p be ArgumentSeq of Sym o,X; :: thesis: ( ( for t being Term of S,X st t in rng p holds
S₁[t] ) implies S₁[[o,the carrier of S] -tree p] )
assume A3: for t being Term of S,X st t in rng p holds
S variables_in t c= X ; :: thesis: S₁[[o,the carrier of S] -tree p]
thus S variables_in ([o,the carrier of S] -tree p) c= X :: thesis: verum

proof

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

end;

end;

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