A2: dom (doms p) = dom p by A1, TREES_3:39;
reconsider q = doms p as Tree-yielding FinSequence by A1;
defpred S₁[ set , set ] means ( ( $1 = {} & $2 = x ) or ( $1 <> {} & ex n being Element of NAT ex r being FinSequence st
( $1 = <*n*> ^ r & $2 = p .. (n + 1),r ) ) );
A3: for y being set st y in tree q holds
ex z being set st S₁[y,z]

proof

let y be set ; :: thesis: ( y in tree q implies ex z being set st S₁[y,z] )
assume A4: y in tree q ; :: thesis: ex z being set st S₁[y,z]
reconsider s = y as Element of tree q by A4;

A5: now

assume A6: y <> {} ; :: thesis: ex z being set st
( ( y = {} & z = x ) or ( y <> {} & ex n being Element of NAT ex r being FinSequence st
( y = <*n*> ^ r & z = p .. (n + 1),r ) ) )
consider w being FinSequence of NAT , n being Nat such that
A7: s = <*n*> ^ w by A6, FINSEQ_2:150;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
reconsider w = w as FinSequence ;
take z = p .. (n + 1),w; :: thesis: ( ( y = {} & z = x ) or ( y <> {} & ex n being Element of NAT ex r being FinSequence st
( y = <*n*> ^ r & z = p .. (n + 1),r ) ) )
thus ( ( y = {} & z = x ) or ( y <> {} & ex n being Element of NAT ex r being FinSequence st
( y = <*n*> ^ r & z = p .. (n + 1),r ) ) ) by A7; :: thesis: verum

end;

thus ex z being set st S₁[y,z] by A5; :: thesis: verum

end;

consider T being Function such that
A8: ( dom T = tree q & ( for y being set st y in tree q holds
S₁[y,T . y] ) ) from CLASSES1:sch 1(A3);
reconsider T = T as DecoratedTree by A8, 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 Element of 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, A8; :: thesis: ( T . {} = x & ( for n being Element of NAT st n < len p holds
T | <*n*> = p . (n + 1) ) )
A9: {} in tree q by TREES_1:47;
thus T . {} = x by A8, A9; :: thesis: for n being Element of NAT st n < len p holds
T | <*n*> = p . (n + 1)
A10: len p = len q by A2, FINSEQ_3:31;
let n be Element of NAT ; :: thesis: ( n < len p implies T | <*n*> = p . (n + 1) )
assume A11: n < len p ; :: thesis: T | <*n*> = p . (n + 1)
A12: n + 1 in dom p by A11, Lm2;
reconsider t = p . (n + 1) as DecoratedTree by A1, A12, TREES_3:26;
A13: dom t = q . (n + 1) by A12, FUNCT_6:31;
A14: dom t = q . (n + 1) by A12, FUNCT_6:31
.= (dom T) | <*n*> by A8, A10, A11, TREES_3:52 ;
A15: (dom T) | <*n*> = dom (T | <*n*>) by TREES_2:def 11;

A16: now

let r be FinSequence of NAT ; :: thesis: ( r in dom t implies (T | <*n*>) . r = t . r )
assume A17: r in dom t ; :: thesis: (T | <*n*>) . r = t . r
A18: <*n*> ^ r in dom T by A8, A10, A11, A13, A17, TREES_3:def 15;
consider m being Element of NAT , s being FinSequence such that
A19: <*n*> ^ r = <*m*> ^ s and
A20: T . (<*n*> ^ r) = p .. (m + 1),s by A8, A18;
A21: ( (<*n*> ^ r) . 1 = n & (<*m*> ^ s) . 1 = m ) by FINSEQ_1:58;
A22: ( m + 1 in dom p & r = s ) by A11, A19, A21, Lm2, FINSEQ_1:46;
A23: p .. (m + 1),s = t . r by A17, A19, A21, A22, FUNCT_5:45;
thus (T | <*n*>) . r = t . r by A14, A17, A20, A23, TREES_2:def 11; :: thesis: verum

end;

thus T | <*n*> = p . (n + 1) by A14, A15, A16, TREES_2:33; :: thesis: verum