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

proof

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

now :: thesis: ( ex n being Nat st
( z = <*n*> & n < len p ) implies ex y being set ex n being Nat st
( z = <*n*> & y = p . (n + 1) ) )

given n being Nat such that A3: z = <*n*> and
n < len p ; :: thesis: ex y being set ex n being Nat st
( z = <*n*> & y = p . (n + 1) )
take y = p . (n + 1); :: thesis: ex n being 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 A3; :: thesis: verum

end;

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

end;

consider f being Function such that
A4: ( dom f = elementary_tree (len p) & ( for y being object st y in elementary_tree (len p) holds
S₁[y,f . y] ) ) from CLASSES1:sch 1(A1);
reconsider f = f as DecoratedTree by A4, TREES_2:def 8;
take f ; :: thesis: ( dom f = elementary_tree (len p) & f . {} = x & ( for n being Nat st n < len p holds
f . <*n*> = p . (n + 1) ) )
thus dom f = elementary_tree (len p) by A4; :: thesis: ( f . {} = x & ( for n being Nat st n < len p holds
f . <*n*> = p . (n + 1) ) )
( {} in dom f & ( for n being Nat st {} = <*n*> holds
f . {} <> p . (n + 1) ) ) by TREES_1:22;
hence f . {} = x by A4; :: thesis: for n being Nat st n < len p holds
f . <*n*> = p . (n + 1)
let n be 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 by A4, TREES_1:28;
then consider k being Nat such that
A5: <*n*> = <*k*> and
A6: f . <*n*> = p . (k + 1) by A4;
k = <*n*> . 1 by A5, FINSEQ_1:40
.= n ;
hence f . <*n*> = p . (n + 1) by A6; :: thesis: verum