defpred S_{1}[ 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_{1}[z,y]

A4: ( dom f = elementary_tree (len p) & ( for y being object st y in elementary_tree (len p) holds

S_{1}[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 by FINSEQ_1:40 ;

hence f . <*n*> = p . (n + 1) by A6; :: thesis: verum

( $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

proof

consider f being Function such that
let z be object ; :: thesis: ( z in elementary_tree (len p) implies ex y being object st S_{1}[z,y] )

assume z in elementary_tree (len p) ; :: thesis: ex y being object st S_{1}[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;

_{1}[z,y]
by A2; :: thesis: verum

end;assume z in elementary_tree (len p) ; :: thesis: ex y being object st S

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) ) )

hence
ex y being object st S( 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;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

A4: ( dom f = elementary_tree (len p) & ( for y being object st y in elementary_tree (len p) holds

S

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 by FINSEQ_1:40 ;

hence f . <*n*> = p . (n + 1) by A6; :: thesis: verum