let x be set ; :: thesis:
let S be non void Signature; :: thesis:
let X be V6 ManySortedSet of the carrier of S; :: thesis:
let t be Element of (Free S,X); :: thesis:
let s be SortSymbol of S; :: thesis:
set Y = X \/ (the carrier of S --> {0 });

hereby :: thesis:

assume x in (S variables_in t) . s ; :: thesis:
then x in { (a `1 ) where a is Element of rng t : a `2 = s } by Def3;
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 Th9;
hence [x,s] in rng t by A1, Th35; :: thesis:

end;

assume A2: [x,s] in rng t ; :: thesis:
then consider z being set such that
A3: ( z in dom t & [x,s] = t . z ) by FUNCT_1:def 5;
reconsider z = z as Element of dom t by A3;
reconsider q = t | z as Element of (Free S,X) by Th34;
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 A4: not [x,s] in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:106;
A5: ( [x,s] = q . {} & q is Term of S,(X \/ (the carrier of S --> {0 })) ) by A3, Th9, QC_LANG4:8;
then consider s' being SortSymbol of S, v being Element of (X \/ (the carrier of S --> {0 })) . s' such that
A6: [x,s] = [v,s'] by A4, MSATERM:2;
A7: ( [x,s] `1 = x & [x,s] `2 = s ) by MCART_1:7;
q = root-tree [v,s'] by A5, A6, MSATERM:5;
then A8: (S variables_in q) . s' = {v} by Th11;
S variables_in q c= X by Th28;
then (S variables_in q) . s' c= X . s' by PBOOLE:def 5;
then A9: ( v in X . s' & x = v & s = s' ) by A6, A8, ZFMISC_1:33, ZFMISC_1:37;
x in { (a `1 ) where a is Element of rng t : a `2 = s } by A2, A7;
hence ( x in (S variables_in t) . s & x in X . s ) by A9, Def3; :: thesis: