defpred S₁[ non empty Relation] means for s being SortSymbol of S holds (S variables_in S) . s is finite ;
A1: for z being SortSymbol of S
for v being Element of X . z holds S₁[ root-tree [v,z]]

proof

let z be SortSymbol of S; :: thesis: for v being Element of X . z holds S₁[ root-tree [v,z]]
let v be Element of X . z; :: thesis: S₁[ root-tree [v,z]]
let s be SortSymbol of S; :: thesis: (S variables_in (root-tree [v,z])) . s is finite
( s = z or s <> z ) ;
hence (S variables_in (root-tree [v,z])) . s is finite by MSAFREE3:10; :: thesis: verum

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
for s being SortSymbol of S holds (S variables_in t) . s is finite ; :: thesis: S₁[[o, the carrier of S] -tree p]
let s be SortSymbol of S; :: thesis: (S variables_in ([o, the carrier of S] -tree p)) . s is finite
deffunc H₂( Term of S,X) -> set = (S variables_in S) . s;
set A = { H₂(q) where q is Term of S,X : q in rng p } ;
A4: rng p is finite ;
A5: { H₂(q) where q is Term of S,X : q in rng p } is finite from FRAENKEL:sch 21(A4);

now :: thesis: for B being set st B in { H₂(q) where q is Term of S,X : q in rng p } holds
B is finite

let B be set ; :: thesis: ( B in { H₂(q) where q is Term of S,X : q in rng p } implies B is finite )
assume B in { H₂(q) where q is Term of S,X : q in rng p } ; :: thesis: B is finite
then ex q being Term of S,X st
( B = (S variables_in q) . s & q in rng p ) ;
hence B is finite by A3; :: thesis: verum

end;

then A6: union { H₂(q) where q is Term of S,X : q in rng p } is finite by A5, FINSET_1:7;
(S variables_in ([o, the carrier of S] -tree p)) . s c= union { H₂(q) where q is Term of S,X : q in rng p }

proof

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 union { H₂(q) where q is Term of S,X : q in rng p } )
assume x in (S variables_in ([o, the carrier of S] -tree p)) . s ; :: thesis: x in union { H₂(q) where q is Term of S,X : q in rng p }
then consider t being DecoratedTree such that
A7: t in rng p and
A8: x in (S variables_in t) . s by MSAFREE3:11;
consider i being object such that
A9: i in dom p and
A10: t = p . i by A7, FUNCT_1:def 3;
reconsider i = i as Nat by A9;
reconsider t = p . i as Term of S,X by A9, MSATERM:22;
(S variables_in t) . s in { H₂(q) where q is Term of S,X : q in rng p } by A7, A10;
hence x in union { H₂(q) where q is Term of S,X : q in rng p } by A8, A10, TARSKI:def 4; :: thesis: verum

end;

hence (S variables_in ([o, the carrier of S] -tree p)) . s is finite by A6; :: thesis: verum

end;

for t being Term of S,X holds S₁[t] from MSATERM:sch 1(A1, A2);
hence (variables_in t) . s is finite ; :: thesis: verum