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

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

assume A2: for t being Term of S,X st t in rng p holds
S variables_in t c= X ; :: thesis: S1[[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 object ; :: according to PBOOLE:def 2 :: thesis: ( not s in the carrier of S or (S variables_in ([o, the carrier of S] -tree p)) . s c= X . s )
assume A3: s in the carrier of S ; :: thesis: (S variables_in ([o, the carrier of S] -tree p)) . s c= X . s
let x be object ; :: 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
A4: t in rng p and
A5: x in () . s by ;
consider i being object such that
A6: i in dom p and
A7: t = p . i by ;
reconsider i = i as Nat by A6;
reconsider t = p . i as Term of S,X by ;
S variables_in t c= X by A2, A4, A7;
then (S variables_in t) . s c= X . s by A3;
hence x in X . s by A5, A7; :: thesis: verum
end;
end;
A8: for s being SortSymbol of S
for v being Element of X . s holds S1[ root-tree [v,s]]
proof
let s be SortSymbol of S; :: thesis: for v being Element of X . s holds S1[ root-tree [v,s]]
let x be Element of X . s; :: thesis: S1[ root-tree [x,s]]
thus S variables_in (root-tree [x,s]) c= X :: thesis: verum
proof
let y be object ; :: according to PBOOLE:def 2 :: 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
A9: ( y <> s implies (S variables_in (root-tree [x,s])) . y = {} ) by Th10;
(S variables_in (root-tree [x,s])) . s = {x} by Th10;
hence (S variables_in (root-tree [x,s])) . y c= X . y by A9; :: thesis: verum
end;
end;
for t being Term of S,X holds S1[t] from hence variables_in t c= X ; :: thesis: verum