let x, z be set ; :: thesis: for S being ManySortedSign
for X being ManySortedSet of the carrier of S
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
let S be ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
let X be ManySortedSet of the carrier of S; :: thesis: for s being set st s in the carrier of S holds
for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X 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 (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) ) )
assume A1: s in the carrier of S ; :: thesis: for p being DTree-yielding FinSequence holds
( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
let p be DTree-yielding FinSequence; :: thesis: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) )
reconsider q = [z, the carrier of S] -tree p as DecoratedTree ;
(X variables_in q) . s = (X . s) /\ ((S variables_in q) . s) by A1, PBOOLE:def 5;
then A2: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ( x in X . s & x in (S variables_in ([z, the carrier of S] -tree p)) . s ) ) by XBOOLE_0:def 4;
then A3: ( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ( x in X . s & ex t being DecoratedTree st
( t in rng p & x in (S variables_in t) . s ) ) ) by A1, Th11;

hereby :: thesis: ( ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s ) implies x in (X variables_in ([z, the carrier of S] -tree p)) . s )

assume x in (X variables_in ([z, the carrier of S] -tree p)) . s ; :: thesis: ex t being DecoratedTree st
( t in rng p & x in (X variables_in t) . s )
then consider t being DecoratedTree such that
A4: t in rng p and
A5: ( x in X . s & x in (S variables_in t) . s ) by A3;
take t = t; :: thesis: ( t in rng p & x in (X variables_in t) . s )
thus t in rng p by A4; :: thesis: x in (X variables_in t) . s
x in (X . s) /\ ((S variables_in t) . s) by A5, XBOOLE_0:def 4;
hence x in (X variables_in t) . s by A1, PBOOLE:def 5; :: thesis: verum

end;

given t being DecoratedTree such that A6: t in rng p and
A7: x in (X variables_in t) . s ; :: thesis: x in (X variables_in ([z, the carrier of S] -tree p)) . s
A8: (X variables_in t) . s = (X . s) /\ ((S variables_in t) . s) by A1, PBOOLE:def 5;
then x in (S variables_in t) . s by A7, XBOOLE_0:def 4;
hence x in (X variables_in ([z, the carrier of S] -tree p)) . s by A1, A2, A6, A7, A8, Th11, XBOOLE_0:def 4; :: thesis: verum