let x be set ; :: thesis: for S being non void Signature
for X being empty-yielding ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let S be non void Signature; :: thesis: for X being empty-yielding ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let X be empty-yielding ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let t be Element of (Free (S,X)); :: thesis: for s being SortSymbol of S holds
( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
let s be SortSymbol of S; :: thesis: ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )
set Y = X (\/) ( the carrier of S --> {0});

hereby :: thesis: ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) )

assume x in (S variables_in t) . s ; :: thesis: [x,s] in rng t
then x in { (a `1) where a is Element of rng t : a `2 = s } by Def2;
then consider a being Element of rng t such that
A1: ( x = a `1 & a `2 = s ) ;
( t is Term of S,(X (\/) ( the carrier of S --> {0})) & a in rng t ) by Th8;
hence [x,s] in rng t by A1, Th34; :: thesis: verum

end;

assume A2: [x,s] in rng t ; :: thesis: ( x in (S variables_in t) . s & x in X . s )
then consider z being object such that
A3: z in dom t and
A4: [x,s] = t . z by FUNCT_1:def 3;
reconsider z = z as Element of dom t by A3;
reconsider q = t | z as Element of (Free (S,X)) by Th33;
A5: [x,s] = q . {} by A4, TREES_9:35;
( [x,s] `1 = x & [x,s] `2 = s ) ;
then A6: x in { (a `1) where a is Element of rng t : a `2 = s } by A2;
A7: q is Term of S,(X (\/) ( the carrier of S --> {0})) by Th8;
s in the carrier of S ;
then s <> the carrier of S ;
then not s in { the carrier of S} by TARSKI:def 1;
then not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
then consider s9 being SortSymbol of S, v being Element of (X (\/) ( the carrier of S --> {0})) . s9 such that
A8: [x,s] = [v,s9] by A5, A7, MSATERM:2;
S variables_in q c= X by Th27;
then A9: (S variables_in q) . s9 c= X . s9 ;
q = root-tree [v,s9] by A5, A7, A8, MSATERM:5;
then (S variables_in q) . s9 = {v} by Th10;
then A10: v in X . s9 by A9, ZFMISC_1:31;
x = v by A8, XTUPLE_0:1;
hence ( x in (S variables_in t) . s & x in X . s ) by A8, A10, A6, Def2, XTUPLE_0:1; :: thesis: verum