let x, z be set ; 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 ; 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; 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 ; ( 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
; 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; ( 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;
given t being DecoratedTree such that A6:
t in rng p
and
A7:
x in (X variables_in t) . s
; 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; verum