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;

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

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 )

given t being DecoratedTree such that A6:
t in rng p
and ( 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;( 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

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