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 ) )

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 ) )

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 ) ) )

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 ) )

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 ) )

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

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 ;
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 ;
( 1 <= n + 1 & n + 1 <= len (doms p) ) by ;
then A13: n + 1 in dom (doms p) by FINSEQ_3:25;
then reconsider t = p . (n + 1) as DecoratedTree by ;
reconsider r = r as FinSequence of NAT by ;
take t = t; :: thesis: ( t in rng p & x in () . s )
thus t in rng p by ; :: thesis: x in () . s
A14: (doms p) . (n + 1) = dom t by ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A15: t = q | <*n*> by ;
then dom t = (dom q) | <*n*> by TREES_2:def 10;
then a = t . r by ;
then a in rng t by ;
then x in { (b `1) where b is Element of rng t : b `2 = s } by A6, A7;
hence x in () . s by ; :: thesis: verum
end;
given t being DecoratedTree such that A16: t in rng p and
A17: x in () . 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 ;
reconsider y = y as Element of NAT by A18;
y >= 1 by ;
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 ;
then A21: n < len p by ;
then A22: t = q | <*n*> by ;
A23: ( {} in dom t & <*n*> ^ {} = <*n*> ) by ;
dom t = (doms p) . (n + 1) by ;
then <*n*> in dom q by ;
then A24: rng t c= rng q by ;
x in { (b `1) where b is Element of rng t : b `2 = s } by ;
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