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 ;

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 (X variables_in t) = the carrier of S by PARTFUN1:def 2;

then s9 in the carrier of S by A5, FUNCT_1:def 2;

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 A5, XBOOLE_0:def 4;

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

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 = {}

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

assume A1:
x in X . s
; :: thesis: (X variables_in (root-tree [x,s])) . s = {x}

then A2: {x} c= X . s by ZFMISC_1:31;

dom X = the carrier of S by PARTFUN1:def 2;

then A3: s in the carrier of S by A1, FUNCT_1:def 2;

then (S variables_in (root-tree [x,s])) . s = {x} by Th10;

then (X . s) /\ ((S variables_in (root-tree [x,s])) . s) = {x} by A2, XBOOLE_1:28;

hence (X variables_in (root-tree [x,s])) . s = {x} by A3, PBOOLE:def 5; :: thesis: verum

end;then A2: {x} c= X . s by ZFMISC_1:31;

dom X = the carrier of S by PARTFUN1:def 2;

then A3: s in the carrier of S by A1, FUNCT_1:def 2;

then (S variables_in (root-tree [x,s])) . s = {x} by Th10;

then (X . s) /\ ((S variables_in (root-tree [x,s])) . s) = {x} by A2, XBOOLE_1:28;

hence (X variables_in (root-tree [x,s])) . s = {x} by A3, PBOOLE:def 5; :: thesis: verum

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 (X variables_in t) = the carrier of S by PARTFUN1:def 2;

then s9 in the carrier of S by A5, FUNCT_1:def 2;

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 A5, XBOOLE_0:def 4;

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