deffunc H1( Nat) -> set = { i where i is Nat : i < $1 } ;
deffunc H2( set ) -> set = H1(F3($1));
A1: for d being Element of F1()
for k1, k2 being Nat st k1 <= k2 & k2 in H2(d) holds
k1 in H2(d)
proof
let d be Element of F1(); :: thesis: for k1, k2 being Nat st k1 <= k2 & k2 in H2(d) holds
k1 in H2(d)
let k1, k2 be Nat; :: thesis: ( k1 <= k2 & k2 in H2(d) implies k1 in H2(d) )
assume A2: ( k1 <= k2 & k2 in { i where i is Nat : i < F3(d) } ) ; :: thesis: k1 in H2(d)
then ex i being Nat st
( k2 = i & i < F3(d) ) ;
then k1 < F3(d) by A2, XXREAL_0:2;
hence k1 in H2(d) ; :: thesis: verum
end;
consider T being DecoratedTree of F1() such that
A3: ( T . {} = F2() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in H2(T . t) } & ( for n being Nat st n in H2(T . t) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) ) from TREES_2:sch 8(A1);
 take T ; :: thesis: ( T . {} = F2() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k < F3((T . t)) } & ( for n being Nat st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) ) ) )
thus T . {} = F2() by A3; :: thesis: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k < F3((T . t)) } & ( for n being Nat st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) )
let t be Element of dom T; :: thesis: ( succ t = { (t ^ <*k*>) where k is Nat : k < F3((T . t)) } & ( for n being Nat st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n) ) )
A4: succ t = { (t ^ <*k*>) where k is Nat : k in H1(F3((T . t))) } by A3;
thus succ t c= { (t ^ <*i*>) where i is Nat : i < F3((T . t)) } :: according to XBOOLE_0:def 10 :: thesis: ( { (t ^ <*k*>) where k is Nat : k < F3((T . t)) } c= succ t & ( for n being Nat st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((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 < F3((T . t)) } )
assume x in succ t ; :: thesis: x in { (t ^ <*i*>) where i is Nat : i < F3((T . t)) }
then consider l being Nat such that
A5: x = t ^ <*l*> and
A6: l in H1(F3((T . t))) by A4;
ex i being Nat st
( l = i & i < F3((T . t)) ) by A6;
hence x in { (t ^ <*i*>) where i is Nat : i < F3((T . t)) } by A5; :: thesis: verum
end;
thus { (t ^ <*i*>) where i is Nat : i < F3((T . t)) } c= succ t :: thesis: for n being Nat st n < F3((T . t)) holds
T . (t ^ <*n*>) = F4() . ((T . t),n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ <*i*>) where i is Nat : i < F3((T . t)) } or x in succ t )
assume x in { (t ^ <*i*>) where i is Nat : i < F3((T . t)) } ; :: thesis: x in succ t
then consider l being Nat such that
A7: x = t ^ <*l*> and
A8: l < F3((T . t)) ;
l in H1(F3((T . t))) by A8;
hence x in succ t by A4, A7; :: thesis: verum
end;
let n be Nat; :: thesis: ( n < F3((T . t)) implies T . (t ^ <*n*>) = F4() . ((T . t),n) )
assume n < F3((T . t)) ; :: thesis: T . (t ^ <*n*>) = F4() . ((T . t),n)
then n in H1(F3((T . t))) ;
hence T . (t ^ <*n*>) = F4() . ((T . t),n) by A3; :: thesis: verum