let x, z be set ; :: thesis: for S being ManySortedSign

for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

let S be ManySortedSign ; :: thesis: for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

let s be set ; :: thesis: ( s in the carrier of S implies for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) ) )

assume A1: s in the carrier of S ; :: thesis: for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

let p be DTree-yielding FinSequence; :: thesis: ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

reconsider q = [z, the carrier of S] -tree p as DecoratedTree ;

A2: (S variables_in q) . s = { (a `1) where a is Element of rng q : a `2 = s } by A1, Def2;

A3: dom q = tree (doms p) by TREES_4:10;

A4: dom (doms p) = dom p by TREES_3:37;

then A5: len p = len (doms p) by FINSEQ_3:29;

A17: x in (S variables_in t) . s ; :: thesis: x in (S variables_in ([z, the carrier of S] -tree p)) . s

consider y being object such that

A18: y in dom p and

A19: t = p . y by A16, FUNCT_1:def 3;

reconsider y = y as Element of NAT by A18;

y >= 1 by A18, FINSEQ_3:25;

then consider n being Nat such that

A20: y = 1 + n by NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

y <= len p by A18, FINSEQ_3:25;

then A21: n < len p by A20, NAT_1:13;

then A22: t = q | <*n*> by A19, A20, TREES_4:def 4;

A23: ( {} in dom t & <*n*> ^ {} = <*n*> ) by FINSEQ_1:34, TREES_1:22;

dom t = (doms p) . (n + 1) by A18, A19, A20, FUNCT_6:22;

then <*n*> in dom q by A3, A5, A21, A23, TREES_3:def 15;

then A24: rng t c= rng q by A22, TREES_2:32;

x in { (b `1) where b is Element of rng t : b `2 = s } by A1, A17, Def2;

then consider b being Element of rng t such that

A25: ( x = b `1 & b `2 = s ) ;

b in rng t ;

hence x in (S variables_in ([z, the carrier of S] -tree p)) . s by A2, A25, A24; :: thesis: verum

for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

let S be ManySortedSign ; :: thesis: for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

let s be set ; :: thesis: ( s in the carrier of S implies for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) ) )

assume A1: s in the carrier of S ; :: thesis: for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

let p be DTree-yielding FinSequence; :: thesis: ( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

reconsider q = [z, the carrier of S] -tree p as DecoratedTree ;

A2: (S variables_in q) . s = { (a `1) where a is Element of rng q : a `2 = s } by A1, Def2;

A3: dom q = tree (doms p) by TREES_4:10;

A4: dom (doms p) = dom p by TREES_3:37;

then A5: len p = len (doms p) by FINSEQ_3:29;

hereby :: thesis: ( ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) implies x in (S variables_in ([z, the carrier of S] -tree p)) . s )

given t being DecoratedTree such that A16:
t in rng p
and ( t in rng p & x in (S variables_in t) . s ) implies x in (S variables_in ([z, the carrier of S] -tree p)) . s )

assume
x in (S variables_in ([z, the carrier of S] -tree p)) . s
; :: thesis: ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s )

then consider a being Element of rng q such that

A6: x = a `1 and

A7: a `2 = s by A2;

consider y being object such that

A8: y in dom q and

A9: a = q . y by FUNCT_1:def 3;

reconsider y = y as Element of dom q by A8;

( q . {} = [z, the carrier of S] & s <> the carrier of S ) by A1, TREES_4:def 4;

then y <> {} by A7, A9;

then consider n being Nat, r being FinSequence such that

A10: n < len (doms p) and

A11: r in (doms p) . (n + 1) and

A12: y = <*n*> ^ r by A3, TREES_3:def 15;

( 1 <= n + 1 & n + 1 <= len (doms p) ) by A10, NAT_1:11, NAT_1:13;

then A13: n + 1 in dom (doms p) by FINSEQ_3:25;

then reconsider t = p . (n + 1) as DecoratedTree by A4, TREES_3:24;

reconsider r = r as FinSequence of NAT by A12, FINSEQ_1:36;

take t = t; :: thesis: ( t in rng p & x in (S variables_in t) . s )

thus t in rng p by A4, A13, FUNCT_1:def 3; :: thesis: x in (S variables_in t) . s

A14: (doms p) . (n + 1) = dom t by A4, A13, FUNCT_6:22;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A15: t = q | <*n*> by A5, A10, TREES_4:def 4;

then dom t = (dom q) | <*n*> by TREES_2:def 10;

then a = t . r by A9, A11, A12, A15, A14, TREES_2:def 10;

then a in rng t by A11, A14, FUNCT_1:def 3;

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

hence x in (S variables_in t) . s by A1, Def2; :: thesis: verum

end;( t in rng p & x in (S variables_in t) . s )

then consider a being Element of rng q such that

A6: x = a `1 and

A7: a `2 = s by A2;

consider y being object such that

A8: y in dom q and

A9: a = q . y by FUNCT_1:def 3;

reconsider y = y as Element of dom q by A8;

( q . {} = [z, the carrier of S] & s <> the carrier of S ) by A1, TREES_4:def 4;

then y <> {} by A7, A9;

then consider n being Nat, r being FinSequence such that

A10: n < len (doms p) and

A11: r in (doms p) . (n + 1) and

A12: y = <*n*> ^ r by A3, TREES_3:def 15;

( 1 <= n + 1 & n + 1 <= len (doms p) ) by A10, NAT_1:11, NAT_1:13;

then A13: n + 1 in dom (doms p) by FINSEQ_3:25;

then reconsider t = p . (n + 1) as DecoratedTree by A4, TREES_3:24;

reconsider r = r as FinSequence of NAT by A12, FINSEQ_1:36;

take t = t; :: thesis: ( t in rng p & x in (S variables_in t) . s )

thus t in rng p by A4, A13, FUNCT_1:def 3; :: thesis: x in (S variables_in t) . s

A14: (doms p) . (n + 1) = dom t by A4, A13, FUNCT_6:22;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

A15: t = q | <*n*> by A5, A10, TREES_4:def 4;

then dom t = (dom q) | <*n*> by TREES_2:def 10;

then a = t . r by A9, A11, A12, A15, A14, TREES_2:def 10;

then a in rng t by A11, A14, FUNCT_1:def 3;

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

hence x in (S variables_in t) . s by A1, Def2; :: thesis: verum

A17: x in (S variables_in t) . s ; :: thesis: x in (S variables_in ([z, the carrier of S] -tree p)) . s

consider y being object such that

A18: y in dom p and

A19: t = p . y by A16, FUNCT_1:def 3;

reconsider y = y as Element of NAT by A18;

y >= 1 by A18, FINSEQ_3:25;

then consider n being Nat such that

A20: y = 1 + n by NAT_1:10;

reconsider n = n as Element of NAT by ORDINAL1:def 12;

y <= len p by A18, FINSEQ_3:25;

then A21: n < len p by A20, NAT_1:13;

then A22: t = q | <*n*> by A19, A20, TREES_4:def 4;

A23: ( {} in dom t & <*n*> ^ {} = <*n*> ) by FINSEQ_1:34, TREES_1:22;

dom t = (doms p) . (n + 1) by A18, A19, A20, FUNCT_6:22;

then <*n*> in dom q by A3, A5, A21, A23, TREES_3:def 15;

then A24: rng t c= rng q by A22, TREES_2:32;

x in { (b `1) where b is Element of rng t : b `2 = s } by A1, A17, Def2;

then consider b being Element of rng t such that

A25: ( x = b `1 & b `2 = s ) ;

b in rng t ;

hence x in (S variables_in ([z, the carrier of S] -tree p)) . s by A2, A25, A24; :: thesis: verum