deffunc H₁( Nat) -> set = { i where i is Nat : i < $1 } ;
deffunc H₂( set ) -> set = H₁(F₃($1));
A1: for d being Element of F₁()
for k1, k2 being 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 Nat st k1 <= k2 & k2 in H₂(d) holds
k1 in H₂(d)
let k1, k2 be Nat; :: thesis: ( k1 <= k2 & k2 in H₂(d) implies k1 in H₂(d) )
assume A2: ( k1 <= k2 & k2 in { i where i is Nat : i < F₃(d) } ) ; :: thesis: k1 in H₂(d)
then ex i being 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
A3: ( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in H₂(T . t) } & ( for n being 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 Nat : k < F₃((T . t)) } & ( for n being Nat st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) ) ) )
thus T . {} = F₂() by A3; :: thesis: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k < F₃((T . t)) } & ( for n being 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 Nat : k < F₃((T . t)) } & ( for n being Nat st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) )
A4: succ t = { (t ^ <*k*>) where k is Nat : k in H₁(F₃((T . t))) } by A3;
thus succ t c= { (t ^ <*i*>) where i is Nat : i < F₃((T . t)) } :: according to XBOOLE_0:def 10 :: thesis: ( { (t ^ <*k*>) where k is Nat : k < F₃((T . t)) } c= succ t & ( for n being Nat st n < F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) )

proof

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ <*i*>) where i is Nat : i < F₃((T . t)) } or x in succ t )
assume x in { (t ^ <*i*>) where i is Nat : i < F₃((T . t)) } ; :: thesis: x in succ t
then consider l being Nat such that
A7: x = t ^ <*l*> and
A8: l < F₃((T . t)) ;
l in H₁(F₃((T . t))) by A8;
hence x in succ t by A4, A7; :: thesis: verum

end;

let n be 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 A3; :: thesis: verum