defpred S1[ 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 S1[z,y]
proof
let z be object ; :: thesis: ( z in elementary_tree (len p) implies ex y being object st S1[z,y] )
assume z in elementary_tree (len p) ; :: thesis: ex y being object st S1[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 S1[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
S1[y,f . y] ) ) from reconsider f = f as DecoratedTree by ;
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 ;
then consider k being Nat such that
A5: <*n*> = <*k*> and
A6: f . <*n*> = p . (k + 1) by A4;
k = <*n*> . 1 by
.= n by FINSEQ_1:40 ;
hence f . <*n*> = p . (n + 1) by A6; :: thesis: verum