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 variables_in t) . 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 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 (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
; :: 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 variables_in t) . 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 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, Def3;
A3:
dom q = tree (doms p)
by TREES_4:10;
A4:
dom (doms p) = dom p
by TREES_3:39;
then A5:
len p = len (doms p)
by FINSEQ_3:31;
hereby :: thesis: ( 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
;
:: thesis: 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 &
a `2 = s )
by A2;
consider y being
set such that A7:
(
y in dom q &
a = q . y )
by FUNCT_1:def 5;
reconsider y =
y as
Element of
dom q by A7;
(
q . {} = [z,the carrier of S] &
s <> the
carrier of
S )
by A1, TREES_4:def 4;
then
y <> {}
by A6, A7, MCART_1:7;
then consider n being
Element of
NAT ,
r being
FinSequence such that A8:
(
n < len (doms p) &
r in (doms p) . (n + 1) &
y = <*n*> ^ r )
by A3, TREES_3:def 15;
reconsider r =
r as
FinSequence of
NAT by A8, FINSEQ_1:50;
( 1
<= n + 1 &
n + 1
<= len (doms p) )
by A8, NAT_1:11, NAT_1:13;
then A9:
n + 1
in dom (doms p)
by FINSEQ_3:27;
then reconsider t =
p . (n + 1) as
DecoratedTree by A4, TREES_3:26;
take t =
t;
:: thesis: ( t in rng p & x in (S variables_in t) . s )thus
t in rng p
by A4, A9, FUNCT_1:def 5;
:: thesis: x in (S variables_in t) . sA10:
(
t = q | <*n*> &
(doms p) . (n + 1) = dom t )
by A4, A5, A8, A9, FUNCT_6:31, TREES_4:def 4;
then
dom t = (dom q) | <*n*>
by TREES_2:def 11;
then
a = t . r
by A7, A8, A10, TREES_2:def 11;
then
a in rng t
by A8, A10, FUNCT_1:def 5;
then
x in { (b `1 ) where b is Element of rng t : b `2 = s }
by A6;
hence
x in (S variables_in t) . s
by A1, Def3;
:: thesis: verum
end;
given t being DecoratedTree such that A11:
( t in rng p & x in (S variables_in t) . s )
; :: thesis: x in (S variables_in ([z,the carrier of S] -tree p)) . s
x in { (b `1 ) where b is Element of rng t : b `2 = s }
by A1, A11, Def3;
then consider b being Element of rng t such that
A12:
( x = b `1 & b `2 = s )
;
consider y being set such that
A13:
( y in dom p & t = p . y )
by A11, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A13;
y >= 1
by A13, FINSEQ_3:27;
then consider n being Nat such that
A14:
y = 1 + n
by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
y <= len p
by A13, FINSEQ_3:27;
then A15:
n < len p
by A14, NAT_1:13;
then A16:
t = q | <*n*>
by A13, A14, TREES_4:def 4;
( {} in dom t & dom t = (doms p) . (n + 1) & <*n*> ^ {} = <*n*> )
by A13, A14, FINSEQ_1:47, FUNCT_6:31, TREES_1:47;
then
<*n*> in dom q
by A3, A5, A15, TREES_3:def 15;
then
( rng t c= rng q & b in rng t )
by A16, TREES_2:34;
hence
x in (S variables_in ([z,the carrier of S] -tree p)) . s
by A2, A12; :: thesis: verum