let x be set ; :: thesis: for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let S be non void Signature; :: thesis: for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let X be V9() ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let t be Element of (Free (S,X)); :: thesis: for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let s be SortSymbol of S; :: thesis: ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

set Y = X (\/) ( the carrier of S --> {0});

then consider z being object such that

A3: z in dom t and

A4: [x,s] = t . z by FUNCT_1:def 3;

reconsider z = z as Element of dom t by A3;

reconsider q = t | z as Element of (Free (S,X)) by Th33;

A5: [x,s] = q . {} by A4, TREES_9:35;

( [x,s] `1 = x & [x,s] `2 = s ) ;

then A6: x in { (a `1) where a is Element of rng t : a `2 = s } by A2;

A7: q is Term of S,(X (\/) ( the carrier of S --> {0})) by Th8;

s in the carrier of S ;

then s <> the carrier of S ;

then not s in { the carrier of S} by TARSKI:def 1;

then not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;

then consider s9 being SortSymbol of S, v being Element of (X (\/) ( the carrier of S --> {0})) . s9 such that

A8: [x,s] = [v,s9] by A5, A7, MSATERM:2;

S variables_in q c= X by Th27;

then A9: (S variables_in q) . s9 c= X . s9 ;

q = root-tree [v,s9] by A5, A7, A8, MSATERM:5;

then (S variables_in q) . s9 = {v} by Th10;

then A10: v in X . s9 by A9, ZFMISC_1:31;

x = v by A8, XTUPLE_0:1;

hence ( x in (S variables_in t) . s & x in X . s ) by A8, A10, A6, Def2, XTUPLE_0:1; :: thesis: verum

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let S be non void Signature; :: thesis: for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let X be V9() ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let t be Element of (Free (S,X)); :: thesis: for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

let s be SortSymbol of S; :: thesis: ( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

set Y = X (\/) ( the carrier of S --> {0});

hereby :: thesis: ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) )

assume A2:
[x,s] in rng t
; :: thesis: ( x in (S variables_in t) . s & x in X . s )assume
x in (S variables_in t) . s
; :: thesis: [x,s] in rng t

then x in { (a `1) where a is Element of rng t : a `2 = s } by Def2;

then consider a being Element of rng t such that

A1: ( x = a `1 & a `2 = s ) ;

( t is Term of S,(X (\/) ( the carrier of S --> {0})) & a in rng t ) by Th8;

hence [x,s] in rng t by A1, Th34; :: thesis: verum

end;then x in { (a `1) where a is Element of rng t : a `2 = s } by Def2;

then consider a being Element of rng t such that

A1: ( x = a `1 & a `2 = s ) ;

( t is Term of S,(X (\/) ( the carrier of S --> {0})) & a in rng t ) by Th8;

hence [x,s] in rng t by A1, Th34; :: thesis: verum

then consider z being object such that

A3: z in dom t and

A4: [x,s] = t . z by FUNCT_1:def 3;

reconsider z = z as Element of dom t by A3;

reconsider q = t | z as Element of (Free (S,X)) by Th33;

A5: [x,s] = q . {} by A4, TREES_9:35;

( [x,s] `1 = x & [x,s] `2 = s ) ;

then A6: x in { (a `1) where a is Element of rng t : a `2 = s } by A2;

A7: q is Term of S,(X (\/) ( the carrier of S --> {0})) by Th8;

s in the carrier of S ;

then s <> the carrier of S ;

then not s in { the carrier of S} by TARSKI:def 1;

then not [x,s] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;

then consider s9 being SortSymbol of S, v being Element of (X (\/) ( the carrier of S --> {0})) . s9 such that

A8: [x,s] = [v,s9] by A5, A7, MSATERM:2;

S variables_in q c= X by Th27;

then A9: (S variables_in q) . s9 c= X . s9 ;

q = root-tree [v,s9] by A5, A7, A8, MSATERM:5;

then (S variables_in q) . s9 = {v} by Th10;

then A10: v in X . s9 by A9, ZFMISC_1:31;

x = v by A8, XTUPLE_0:1;

hence ( x in (S variables_in t) . s & x in X . s ) by A8, A10, A6, Def2, XTUPLE_0:1; :: thesis: verum