let S be ManySortedSign ; :: thesis:
let s, x be set ; :: thesis:
reconsider t = root-tree [x,s] as DecoratedTree ;
t = {[{} ,[x,s]]} by TREES_4:6;
then A1: rng t = {[x,s]} by RELAT_1:23;
A2: ( [x,s] `1 = x & [x,s] `2 = s ) by MCART_1:7;

hereby :: thesis:

assume s in the carrier of S ; :: thesis:
then A3: (S variables_in t) . s = { (a `1 ) where a is Element of rng t : a `2 = s } by Def3;
thus (S variables_in (root-tree [x,s])) . s = {x} :: thesis:

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

let y be set ; :: thesis:
assume y in (S variables_in (root-tree [x,s])) . s ; :: thesis:
then consider a being Element of rng t such that
A4: ( y = a `1 & a `2 = s ) by A3;
a = [x,s] by A1, TARSKI:def 1;
hence y in {x} by A2, A4, TARSKI:def 1; :: thesis:

end;

[x,s] in rng t by A1, TARSKI:def 1;
then x in { (a `1 ) where a is Element of rng t : a `2 = s } by A2;
hence {x} c= (S variables_in (root-tree [x,s])) . s by A3, ZFMISC_1:37; :: thesis:

end;

end;

let s' be set ; :: thesis:
assume A5: ( s' <> s or not s in the carrier of S ) ; :: thesis:
consider y being Element of (S variables_in (root-tree [x,s])) . s';
assume A6: (S variables_in (root-tree [x,s])) . s' <> {} ; :: thesis:
then A7: y in (S variables_in t) . s' ;
dom (S variables_in t) = the carrier of S by PARTFUN1:def 4;
then A8: s' in the carrier of S by A6, FUNCT_1:def 4;
then (S variables_in t) . s' = { (a `1 ) where a is Element of rng t : a `2 = s' } by Def3;
then consider a being Element of rng t such that
A9: ( y = a `1 & a `2 = s' ) by A7;
thus contradiction by A1, A2, A5, A8, A9, TARSKI:def 1; :: thesis: