set A = [:NAT ,NAT :];
defpred S₁[ set ] means ( $1 is finite DecoratedTree of & ( for y being finite DecoratedTree of st y = $1 holds
( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) ) ) ) );
consider Y being set such that
A1: for x being set holds
( x in Y iff ( x in PFuncs (NAT * ),[:NAT ,NAT :] & S₁[x] ) ) from XBOOLE_0:sch 1();
A2: for x being finite DecoratedTree of holds
( x in Y iff ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) )

proof

let x be finite DecoratedTree of ; :: thesis: ( x in Y iff ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) )
thus ( x in Y implies ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) ) by A1; :: thesis: ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) implies x in Y )
assume ( dom x is finite & ( for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) ; :: thesis: x in Y
then A3: for y being finite DecoratedTree of st y = x holds
( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) ) ) ;
x in PFuncs (NAT * ),[:NAT ,NAT :] by Th13;
hence x in Y by A1, A3; :: thesis: verum

end;

set t = elementary_tree 0 ;
deffunc H₁( set ) -> Element of [:NAT ,NAT :] = [0 ,0 ];
consider T being DecoratedTree such that
A4: ( dom T = elementary_tree 0 & ( for p being FinSequence of NAT st p in elementary_tree 0 holds
T . p = H₁(p) ) ) from TREES_2:sch 7();
rng T c= [:NAT ,NAT :]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng T or x in [:NAT ,NAT :] )
assume x in rng T ; :: thesis: x in [:NAT ,NAT :]
then consider z being set such that
A5: ( z in dom T & x = T . z ) by FUNCT_1:def 5;
z = <*> NAT by A4, A5, TARSKI:def 1, TREES_1:56;
then reconsider z = z as FinSequence of NAT ;
T . z = [0 ,0 ] by A4, A5;
hence x in [:NAT ,NAT :] by A5; :: thesis: verum

end;

then reconsider T = T as finite DecoratedTree of by A4, Lm2, RELAT_1:def 19;
A6: T in PFuncs (NAT * ),[:NAT ,NAT :] by Th13;
for y being finite DecoratedTree of st y = T holds
( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) ) )

proof

let y be finite DecoratedTree of ; :: thesis: ( y = T implies ( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) ) ) )
assume A7: y = T ; :: thesis: ( dom y is finite & ( for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) ) )
thus dom y is finite ; :: thesis: for v being Element of dom y holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) )
let v be Element of dom y; :: thesis: ( branchdeg v <= 2 & ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) )
A8: succ v = {}

proof

A9: succ v = { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in dom y } by TREES_2:def 5;
assume A10: not succ v = {} ; :: thesis: contradiction
consider x being Element of succ v;
x in succ v by A10;
then consider n being Element of NAT such that
A11: ( x = v ^ <*n*> & v ^ <*n*> in dom y ) by A9;
thus contradiction by A4, A7, A11, TARSKI:def 1, TREES_1:56; :: thesis: verum

end;

hence branchdeg v <= 2 by CARD_1:47, TREES_2:def 13; :: thesis: ( ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) )
thus ( ( not branchdeg v = 0 or y . v = [0 ,0 ] or ex k being Element of NAT st y . v = [3,k] ) & ( not branchdeg v = 1 or y . v = [1,0 ] or y . v = [1,1] ) & ( branchdeg v = 2 implies y . v = [2,0 ] ) ) by A4, A7, A8, CARD_1:47, TREES_2:def 13; :: thesis: verum

end;

then reconsider Y = Y as non empty set by A1, A6;
for x being set st x in Y holds
x is DecoratedTree of by A1;
then reconsider Y = Y as DOMAIN_DecoratedTree of [:NAT ,NAT :] by Def5;
take Y ; :: thesis: ( ( for x being DecoratedTree of st x in Y holds
x is finite ) & ( for x being finite DecoratedTree of holds
( x in Y iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) )
thus ( ( for x being DecoratedTree of st x in Y holds
x is finite ) & ( for x being finite DecoratedTree of holds
( x in Y iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0 ,0 ] or ex k being Element of NAT st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0 ] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0 ] ) ) ) ) ) by A1, A2; :: thesis: verum