let S be ManySortedSign ; :: thesis: for s, x being object holds
( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being object st ( s9 <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s9 = {} ) )
let s, x be object ; :: thesis: ( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being object st ( s9 <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s9 = {} ) )
reconsider t = root-tree [x,s] as DecoratedTree ;
A1: [x,s] `2 = s ;
t = {[{},[x,s]]} by TREES_4:6;
then A2: rng t = {[x,s]} by RELAT_1:9;
A3: [x,s] `1 = x ;

hereby :: thesis: for s9 being object st ( s9 <> s or not s in the carrier of S ) holds
(S variables_in (root-tree [x,s])) . s9 = {}

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

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {x} c= (S variables_in (root-tree [x,s])) . s

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

end;

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

end;

end;

let s9 be object ; :: thesis: ( ( s9 <> s or not s in the carrier of S ) implies (S variables_in (root-tree [x,s])) . s9 = {} )
assume A6: ( s9 <> s or not s in the carrier of S ) ; :: thesis: (S variables_in (root-tree [x,s])) . s9 = {}
set y = the Element of (S variables_in (root-tree [x,s])) . s9;
assume A7: (S variables_in (root-tree [x,s])) . s9 <> {} ; :: thesis: contradiction
then A8: the Element of (S variables_in (root-tree [x,s])) . s9 in (S variables_in t) . s9 ;
dom (S variables_in t) = the carrier of S by PARTFUN1:def 2;
then A9: s9 in the carrier of S by A7, FUNCT_1:def 2;
then (S variables_in t) . s9 = { (a `1) where a is Element of rng t : a `2 = s9 } by Def2;
then ex a being Element of rng t st
( the Element of (S variables_in (root-tree [x,s])) . s9 = a `1 & a `2 = s9 ) by A8;
hence contradiction by A2, A1, A6, A9, TARSKI:def 1; :: thesis: verum