reconsider pp = p as Function-yielding FinSequence by A1;
A2:
dom (doms pp) = dom p
by A1, TREES_3:37;
reconsider q = doms pp as Tree-yielding FinSequence by A1;
defpred S1[ object , object ] means ( ( $1 = {} & $2 = x ) or ( $1 <> {} & ex n being Nat ex r being FinSequence st
( $1 = <*n*> ^ r & $2 = p .. ((n + 1),r) ) ) );
A3:
for y being object st y in tree q holds
ex z being object st S1[y,z]
consider T being Function such that
A5:
( dom T = tree q & ( for y being object st y in tree q holds
S1[y,T . y] ) )
from CLASSES1:sch 1(A3);
reconsider T = T as DecoratedTree by A5, TREES_2:def 8;
take
T
; ( ex q being DTree-yielding FinSequence st
( p = q & dom T = tree (doms q) ) & T . {} = x & ( for n being Nat st n < len p holds
T | <*n*> = p . (n + 1) ) )
thus
ex q being DTree-yielding FinSequence st
( p = q & dom T = tree (doms q) )
by A1, A5; ( T . {} = x & ( for n being Nat st n < len p holds
T | <*n*> = p . (n + 1) ) )
{} in tree q
by TREES_1:22;
hence
T . {} = x
by A5; for n being Nat st n < len p holds
T | <*n*> = p . (n + 1)
A6:
len p = len q
by A2, FINSEQ_3:29;
let n be Nat; ( n < len p implies T | <*n*> = p . (n + 1) )
assume A7:
n < len p
; T | <*n*> = p . (n + 1)
then A8:
n + 1 in dom p
by Lm2;
then reconsider t = p . (n + 1) as DecoratedTree by A1, TREES_3:24;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A9:
dom t = q . (n + 1)
by A8, FUNCT_6:22;
A10: dom t =
q . (n + 1)
by A8, FUNCT_6:22
.=
(dom T) | <*nn*>
by A5, A6, A7, TREES_3:49
;
A11:
(dom T) | <*n*> = dom (T | <*n*>)
by TREES_2:def 10;
now for r being FinSequence of NAT st r in dom t holds
(T | <*n*>) . r = t . rlet r be
FinSequence of
NAT ;
( r in dom t implies (T | <*n*>) . r = t . r )assume A12:
r in dom t
;
(T | <*n*>) . r = t . rthen
<*n*> ^ r in dom T
by A5, A6, A7, A9, TREES_3:def 15;
then consider m being
Nat,
s being
FinSequence such that A13:
<*n*> ^ r = <*m*> ^ s
and A14:
T . (<*n*> ^ r) = p .. (
(m + 1),
s)
by A5;
A15:
(
(<*n*> ^ r) . 1
= n &
(<*m*> ^ s) . 1
= m )
by FINSEQ_1:41;
then
(
m + 1
in dom p &
r = s )
by A7, A13, Lm2, FINSEQ_1:33;
then
p .. (
(m + 1),
s)
= t . r
by A12, A13, A15, FUNCT_5:38;
hence
(T | <*n*>) . r = t . r
by A10, A12, A14, TREES_2:def 10;
verum end;
hence
T | <*n*> = p . (n + 1)
by A10, A11, TREES_2:31; verum