deffunc H₁( set ) -> Element of [:omega,omega:] = [0,0];
set t = elementary_tree 0;
set A = [:NAT,NAT:];
defpred S₁[ object ] means ( $1 is finite DecoratedTree of [:NAT,NAT:] & ( for y being finite DecoratedTree of [:NAT,NAT:] 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 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 object 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 [:NAT,NAT:] 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 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 [:NAT,NAT:]; :: 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 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 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 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 that
dom x is finite and
A3: for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being 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
A4: x in PFuncs ((NAT *),[:NAT,NAT:]) by Th5;
for y being finite DecoratedTree of [:NAT,NAT:] 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 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 A3;
hence x in Y by A1, A4; :: thesis: verum

end;

consider T being DecoratedTree such that
A5: ( 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 object ; :: 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 object such that
A6: z in dom T and
A7: x = T . z by FUNCT_1:def 3;
z = <*> NAT by A5, A6, TARSKI:def 1, TREES_1:29;
then reconsider z = z as FinSequence of NAT ;
T . z = [0,0] by A5, A6;
hence x in [:NAT,NAT:] by A7; :: thesis: verum

end;

then reconsider T = T as finite DecoratedTree of [:NAT,NAT:] by A5, Lm2, RELAT_1:def 19;
A8: for y being finite DecoratedTree of [:NAT,NAT:] 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 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 [:NAT,NAT:]; :: 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 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 A9: 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 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 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 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] ) )
A10: succ v = {}

proof

set x = the Element of succ v;
assume not succ v = {} ; :: thesis: contradiction
then A11: the Element of succ v in succ v ;
succ v = { (v ^ <*n*>) where n is Nat : v ^ <*n*> in dom y } by TREES_2:def 5;
then ex n being Nat st
( the Element of succ v = v ^ <*n*> & v ^ <*n*> in dom y ) by A11;
hence contradiction by A5, A9, TARSKI:def 1, TREES_1:29; :: thesis: verum

end;

hence branchdeg v <= 2 by CARD_1:27, TREES_2:def 12; :: thesis: ( ( not branchdeg v = 0 or y . v = [0,0] or ex k being 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 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 A5, A9, A10, CARD_1:27, TREES_2:def 12; :: thesis: verum

end;

T in PFuncs ((NAT *),[:NAT,NAT:]) by Th5;
then reconsider Y = Y as non empty set by A1, A8;
for x being object st x in Y holds
x is DecoratedTree of [:NAT,NAT:] by A1;
then reconsider Y = Y as DTree-set of [:NAT,NAT:] by TREES_3:def 6;
take Y ; :: thesis: ( ( for x being DecoratedTree of [:NAT,NAT:] st x in Y holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] 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 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 [:NAT,NAT:] st x in Y holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] 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 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