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 and
A4: [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;
A5: [x,s] = q . {} by A4, QC_LANG4:8;
( [x,s] `1 = x & [x,s] `2 = s ) by MCART_1:7;
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 Th9;
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:106;
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 Th28;
then A9: (S variables_in q) . s9 c= X . s9 by PBOOLE:def 5;
q = root-tree [v,s9] by A5, A7, A8, MSATERM:5;
then (S variables_in q) . s9 = {v} by Th11;
then A10: v in X . s9 by A9, ZFMISC_1:37;
x = v by A8, ZFMISC_1:33;
hence ( x in (S variables_in t) . s & x in X . s ) by A8, A10, A6, Def3, ZFMISC_1:33; :: thesis: