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:11; :: 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 B1: 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 } ;
B2: rng p is finite ;
B3: { H₂(q) where q is Term of S,X : q in rng p } is finite from FRAENKEL:sch 21(B2);

now

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 B1; :: thesis: verum

end;

then B5: union { H₂(q) where q is Term of S,X : q in rng p } is finite by B3, FINSET_1:25;
(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 set ; :: 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
B6: ( t in rng p & x in (S variables_in t) . s ) by MSAFREE3:12;
consider i being set such that
B7: ( i in dom p & t = p . i ) by B6, FUNCT_1:def 5;
reconsider i = i as Nat by B7;
reconsider t = p . i as Term of S,X by B7, MSATERM:22;
(S variables_in t) . s in { H₂(q) where q is Term of S,X : q in rng p } by B6, B7;
hence x in union { H₂(q) where q is Term of S,X : q in rng p } by B6, B7, TARSKI:def 4; :: thesis: verum

end;

hence (S variables_in ([o,the carrier of S] -tree p)) . s is finite by B5; :: 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