let x be set ; :: thesis: for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in () . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in () . s & x in X . s ) ) )

let S be non void Signature; :: thesis: for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for s being SortSymbol of S holds
( ( x in () . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in () . s & x in X . s ) ) )

let X be V9() 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 implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in () . s & x in X . s ) ) )

let t be Element of (Free (S,X)); :: thesis: for s being SortSymbol of S holds
( ( x in () . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in () . s & x in X . s ) ) )

let s be SortSymbol of S; :: thesis: ( ( x in () . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in () . s & x in X . s ) ) )
set Y = X (\/) ( the carrier of S --> );
hereby :: thesis: ( [x,s] in rng t implies ( x in () . s & x in X . s ) )
assume x in () . 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 --> )) & a in rng t ) by Th8;
hence [x,s] in rng t by ; :: thesis: verum
end;
assume A2: [x,s] in rng t ; :: thesis: ( x in () . 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 ;
( [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 --> )) 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 --> )) . s9 such that
A8: [x,s] = [v,s9] by ;
S variables_in q c= X by Th27;
then A9: (S variables_in q) . s9 c= X . s9 ;
q = root-tree [v,s9] by ;
then (S variables_in q) . s9 = {v} by Th10;
then A10: v in X . s9 by ;
x = v by ;
hence ( x in () . s & x in X . s ) by ; :: thesis: verum