let S be non void Signature; 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; 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; variables_in t c= X
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;
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);
( ( 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
;
S1[[o, the carrier of S] -tree p]
thus
S variables_in ([o, the carrier of S] -tree p) c= X
verumproof
let s be
object ;
PBOOLE:def 2 ( 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
;
(S variables_in ([o, the carrier of S] -tree p)) . s c= X . s
let x be
object ;
TARSKI:def 3 ( 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
;
x in X . s
then consider t being
DecoratedTree such that A4:
t in rng p
and A5:
x in (S variables_in t) . s
by A3, Th11;
consider i being
object such that A6:
i in dom p
and A7:
t = p . i
by A4, FUNCT_1:def 3;
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 A2, A4, A7;
then
(S variables_in t) . s c= X . s
by A3;
hence
x in X . s
by A5, A7;
verum
end;
end;
A8:
for s being SortSymbol of S
for v being Element of X . s holds S1[ root-tree [v,s]]
for t being Term of S,X holds S1[t]
from MSATERM:sch 1(A8, A1);
hence
variables_in t c= X
; verum