defpred S₁[ set , set ] means ( ( $1 = {} & $2 = x ) or ex n being Element of NAT st
( $1 = <*n*> & $2 = p . (n + 1) ) );
A1: 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 A2: z in elementary_tree (len p) ; :: thesis: ex y being set st S₁[z,y]
reconsider z = z as Element of elementary_tree (len p) by A2;
reconsider z = z as FinSequence of NAT ;
A3: ( z = {} or ex n being Element of NAT st
( n < len p & z = <*n*> ) ) by TREES_1:57;

A4: now

given n being Element of NAT such that A5: z = <*n*> and
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 A5; :: thesis: verum

end;

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

end;

consider f being Function such that
A6: ( 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(A1);
reconsider f = f as DecoratedTree by A6, 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 A6; :: thesis: ( f . {} = x & ( for n being Element of NAT st n < len p holds
f . <*n*> = p . (n + 1) ) )
A7: ( {} in dom f & ( for n being Element of NAT st {} = <*n*> holds
f . {} <> p . (n + 1) ) ) by TREES_1:47;
thus f . {} = x by A6, A7; :: 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 A8: n < len p ; :: thesis: f . <*n*> = p . (n + 1)
A9: <*n*> in dom f by A6, A8, TREES_1:55;
consider k being Element of NAT such that
A10: <*n*> = <*k*> and
A11: f . <*n*> = p . (k + 1) by A6, A9;
A12: k = <*n*> . 1 by A10, FINSEQ_1:57
.= n by FINSEQ_1:57 ;
thus f . <*n*> = p . (n + 1) by A11, A12; :: thesis: verum