let S be ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for s, x being set holds
( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )

let X be ManySortedSet of the carrier of S; :: thesis: for s, x being set holds
( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )

let s, x be set ; :: thesis: ( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {} ) )

reconsider t = root-tree [x,s] as DecoratedTree ;
hereby :: thesis: for s9 being set st ( s9 <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s9 = {}
end;
let s9 be set ; :: thesis: ( ( s9 <> s or not x in X . s ) implies (X variables_in (root-tree [x,s])) . s9 = {} )
assume A4: ( s9 <> s or not x in X . s ) ; :: thesis: (X variables_in (root-tree [x,s])) . s9 = {}
set y = the Element of (X variables_in (root-tree [x,s])) . s9;
assume A5: (X variables_in (root-tree [x,s])) . s9 <> {} ; :: thesis: contradiction
dom () = the carrier of S by PARTFUN1:def 2;
then s9 in the carrier of S by ;
then A6: (X variables_in t) . s9 = (X . s9) /\ { (a `1) where a is Element of rng t : a `2 = s9 } by Th9;
then the Element of (X variables_in (root-tree [x,s])) . s9 in { (a `1) where a is Element of rng t : a `2 = s9 } by ;
then consider a being Element of rng t such that
A7: ( the Element of (X variables_in (root-tree [x,s])) . s9 = a `1 & a `2 = s9 ) ;
t = {[{},[x,s]]} by TREES_4:6;
then rng t = {[x,s]} by RELAT_1:9;
then a = [x,s] by TARSKI:def 1;
hence contradiction by A4, A5, A6, A7, XBOOLE_0:def 4; :: thesis: verum