deffunc H₁( Element of NAT ) -> set = { i where i is Element of NAT : i < $1 } ;
deffunc H₂( set ) -> set = H₁(F₃($1));
A1: for d being Element of F₁()
for k1, k2 being Element of NAT st k1 <= k2 & k2 in H₂(d) holds
k1 in H₂(d)

proof

let d be Element of F₁(); :: thesis: for k1, k2 being Element of NAT st k1 <= k2 & k2 in H₂(d) holds
k1 in H₂(d)
let k1, k2 be Element of NAT ; :: thesis: ( k1 <= k2 & k2 in H₂(d) implies k1 in H₂(d) )
assume A2: ( k1 <= k2 & k2 in { i where i is Element of NAT : i < F₃(d) } ) ; :: thesis: k1 in H₂(d)
then ex i being Element of NAT st
( k2 = i & i < F₃(d) ) ;
then k1 < F₃(d) by A2, XXREAL_0:2;
hence k1 in H₂(d) ; :: thesis: verum

end;

consider T being DecoratedTree of F₁() such that
A5: ( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in H₂(T . t) } & ( for n being Element of NAT st n in H₂(T . t) holds
T . (t ^ <*n*>) = F₄() . (T . t),n ) ) ) ) from TREES_2:sch 8(A1);
take T ; :: thesis: ( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F₃((T . t)) } & ( for n being Element of NAT st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . (T . t),n ) ) ) )
thus T . {} = F₂() by A5; :: thesis: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F₃((T . t)) } & ( for n being Element of NAT st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . (T . t),n ) )
let t be Element of dom T; :: thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k < F₃((T . t)) } & ( for n being Element of NAT st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . (T . t),n ) )
A6: succ t = { (t ^ <*k*>) where k is Element of NAT : k in H₁(F₃((T . t))) } by A5;
thus succ t c= { (t ^ <*i*>) where i is Element of NAT : i < F₃((T . t)) } :: according to XBOOLE_0:def 10 :: thesis: ( { (t ^ <*k*>) where k is Element of NAT : k < F₃((T . t)) } c= succ t & ( for n being Element of NAT st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . (T . t),n ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : i < F₃((T . t)) } )
assume x in succ t ; :: thesis: x in { (t ^ <*i*>) where i is Element of NAT : i < F₃((T . t)) }
then consider l being Element of NAT such that
A8: x = t ^ <*l*> and
A9: l in H₁(F₃((T . t))) by A6;
ex i being Element of NAT st
( l = i & i < F₃((T . t)) ) by A9;
hence x in { (t ^ <*i*>) where i is Element of NAT : i < F₃((T . t)) } by A8; :: thesis: verum

end;

thus { (t ^ <*i*>) where i is Element of NAT : i < F₃((T . t)) } c= succ t :: thesis: for n being Element of NAT st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . (T . t),n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : i < F₃((T . t)) } or x in succ t )
assume x in { (t ^ <*i*>) where i is Element of NAT : i < F₃((T . t)) } ; :: thesis: x in succ t
then consider l being Element of NAT such that
A12: x = t ^ <*l*> and
A13: l < F₃((T . t)) ;
l in H₁(F₃((T . t))) by A13;
hence x in succ t by A6, A12; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( n < F₃((T . t)) implies T . (t ^ <*n*>) = F₄() . (T . t),n )
assume n < F₃((T . t)) ; :: thesis: T . (t ^ <*n*>) = F₄() . (T . t),n
then n in H₁(F₃((T . t))) ;
hence T . (t ^ <*n*>) = F₄() . (T . t),n by A5; :: thesis: verum