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 S_{1}[ 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 S_{1}[y,z]

A5: ( dom T = tree q & ( for y being object st y in tree q holds

S_{1}[y,T . y] ) )
from CLASSES1:sch 1(A3);

reconsider T = T as DecoratedTree by A5, TREES_2:def 8;

take T ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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; :: thesis: ( n < len p implies T | <*n*> = p . (n + 1) )

assume A7: n < len p ; :: thesis: 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;

A2: dom (doms pp) = dom p by A1, TREES_3:37;

reconsider q = doms pp as Tree-yielding FinSequence by A1;

defpred S

( $1 = <*n*> ^ r & $2 = p .. ((n + 1),r) ) ) );

A3: for y being object st y in tree q holds

ex z being object st S

proof

consider T being Function such that
let y be object ; :: thesis: ( y in tree q implies ex z being object st S_{1}[y,z] )

assume y in tree q ; :: thesis: ex z being object st S_{1}[y,z]

then reconsider s = y as Element of tree q ;

_{1}[y,z]
; :: thesis: verum

end;assume y in tree q ; :: thesis: ex z being object st S

then reconsider s = y as Element of tree q ;

now :: thesis: ( y <> {} implies ex z being set st

( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) ) )

hence
ex z being object st S( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) ) )

assume
y <> {}
; :: thesis: ex z being set st

( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) )

then consider w being FinSequence of NAT , n being Element of NAT such that

A4: s = <*n*> ^ w by FINSEQ_2:130;

reconsider w = w as FinSequence ;

take z = p .. ((n + 1),w); :: thesis: ( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) )

thus ( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) ) by A4; :: thesis: verum

end;( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) )

then consider w being FinSequence of NAT , n being Element of NAT such that

A4: s = <*n*> ^ w by FINSEQ_2:130;

reconsider w = w as FinSequence ;

take z = p .. ((n + 1),w); :: thesis: ( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) )

thus ( ( y = {} & z = x ) or ( y <> {} & ex n being Nat ex r being FinSequence st

( y = <*n*> ^ r & z = p .. ((n + 1),r) ) ) ) by A4; :: thesis: verum

A5: ( dom T = tree q & ( for y being object st y in tree q holds

S

reconsider T = T as DecoratedTree by A5, TREES_2:def 8;

take T ; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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; :: thesis: ( n < len p implies T | <*n*> = p . (n + 1) )

assume A7: n < len p ; :: thesis: 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 :: thesis: for r being FinSequence of NAT st r in dom t holds

(T | <*n*>) . r = t . r

hence
T | <*n*> = p . (n + 1)
by A10, A11, TREES_2:31; :: thesis: verum(T | <*n*>) . r = t . r

let r be FinSequence of NAT ; :: thesis: ( r in dom t implies (T | <*n*>) . r = t . r )

assume A12: r in dom t ; :: thesis: (T | <*n*>) . r = t . r

then <*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; :: thesis: verum

end;assume A12: r in dom t ; :: thesis: (T | <*n*>) . r = t . r

then <*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; :: thesis: verum