defpred S₁[ set , set ] means ( ( $1 = {} & $2 = x ) or ex n being Element of NAT st
( $1 = <*n*> & $2 = p . (n + 1) ) );
A8: for z being set st z in elementary_tree (len p) holds
ex y being set st S₁[z,y]

proof

let z be set ; :: thesis: ( z in elementary_tree (len p) implies ex y being set st S₁[z,y] )
assume z in elementary_tree (len p) ; :: thesis: ex y being set st S₁[z,y]
then reconsider z = z as Element of elementary_tree (len p) ;
reconsider z = z as FinSequence of NAT ;
A9: ( z = {} or ex n being Element of NAT st
( n < len p & z = <*n*> ) ) by TREES_1:57;

now

given n being Element of NAT such that A10: ( z = <*n*> & n < len p ) ; :: thesis: ex y being set ex n being Element of NAT st
( z = <*n*> & y = p . (n + 1) )
take y = p . (n + 1); :: thesis: ex n being Element of NAT st
( z = <*n*> & y = p . (n + 1) )
take n = n; :: thesis: ( z = <*n*> & y = p . (n + 1) )
thus ( z = <*n*> & y = p . (n + 1) ) by A10; :: thesis: verum

end;

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

end;

consider f being Function such that
A11: ( dom f = elementary_tree (len p) & ( for y being set st y in elementary_tree (len p) holds
S₁[y,f . y] ) ) from CLASSES1:sch 1(A8);
reconsider f = f as DecoratedTree by A11, TREES_2:def 8;
take f ; :: thesis: ( dom f = elementary_tree (len p) & f . {} = x & ( for n being Element of NAT st n < len p holds
f . <*n*> = p . (n + 1) ) )
thus dom f = elementary_tree (len p) by A11; :: thesis: ( f . {} = x & ( for n being Element of NAT st n < len p holds
f . <*n*> = p . (n + 1) ) )
( {} in dom f & ( for n being Element of NAT st {} = <*n*> holds
f . {} <> p . (n + 1) ) ) by TREES_1:47;
hence f . {} = x by A11; :: thesis: for n being Element of NAT st n < len p holds
f . <*n*> = p . (n + 1)
let n be Element of NAT ; :: thesis: ( n < len p implies f . <*n*> = p . (n + 1) )
assume n < len p ; :: thesis: f . <*n*> = p . (n + 1)
then ( <*n*> in dom f & <*n*> <> {} ) by A11, TREES_1:55;
then consider k being Element of NAT such that
A12: ( <*n*> = <*k*> & f . <*n*> = p . (k + 1) ) by A11;
k = <*n*> . 1 by A12, FINSEQ_1:57
.= n by FINSEQ_1:57 ;
hence f . <*n*> = p . (n + 1) by A12; :: thesis: verum