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 ;

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

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

let s9 be object ; :: thesis: ( ( s9 <> s or not s in the carrier of S ) implies (S variables_in (root-tree [x,s])) . s9 = {} )(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

end;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

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;

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

[x,s] in rng t
by A2, TARSKI:def 1;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;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

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

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