let x, z be set ; 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 ; 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 ; ( 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
; 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; ( 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 ( 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 )
assume
x in (S variables_in ([z, the carrier of S] -tree p)) . s
;
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;
( t in rng p & x in (S variables_in t) . s )thus
t in rng p
by A4, A13, FUNCT_1:def 3;
x in (S variables_in t) . sA14:
(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;
verum
end;
given t being DecoratedTree such that A16:
t in rng p
and
A17:
x in (S variables_in t) . s
; 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; verum