defpred S₁[ object , object ] means ex b, c being Element of F₁() st
( P₁[$1,b,c] & $2 = [b,c] );
A2: for e being object st e in F₁() holds
ex u being object st
( u in [:F₁(),F₁():] & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in F₁() implies ex u being object st
( u in [:F₁(),F₁():] & S₁[e,u] ) )
assume e in F₁() ; :: thesis: ex u being object st
( u in [:F₁(),F₁():] & S₁[e,u] )
then consider b, c being Element of F₁() such that
A3: P₁[e,b,c] by A1;
take u = [b,c]; :: thesis: ( u in [:F₁(),F₁():] & S₁[e,u] )
thus u in [:F₁(),F₁():] ; :: thesis: S₁[e,u]
thus S₁[e,u] by A3; :: thesis: verum

end;

consider f being Function such that
A4: dom f = F₁() and
A5: rng f c= [:F₁(),F₁():] and
A6: for e being object st e in F₁() holds
S₁[e,f . e] from FUNCT_1:sch 6(A2);
deffunc H₁( object ) -> object = IFEQ (($1 `2),0,((f . ($1 `1)) `1),((f . ($1 `1)) `2));
A7: for x being object st x in [:F₁(),NAT:] holds
H₁(x) in F₁()

proof

let x be object ; :: thesis: ( x in [:F₁(),NAT:] implies H₁(x) in F₁() )
assume x in [:F₁(),NAT:] ; :: thesis: H₁(x) in F₁()
then x `1 in F<sub>1</sub>() by MCART_1:10;
then A8: f . (x `1) in rng f by A4, FUNCT_1:def 3;
then A9: (f . (x `1)) `2 in F₁() by A5, MCART_1:10;
A10: (f . (x `1)) `1 in F₁() by A5, A8, MCART_1:10;

now :: thesis: H₁(x) in F₁()

per cases ( x `2 = 0 or x `2 <> 0 ) ;

suppose x `2 = 0 ; :: thesis: H₁(x) in F₁()

hence H₁(x) in F₁() by A10, FUNCOP_1:def 8; :: thesis: verum

end;

suppose x `2 <> 0 ; :: thesis: H₁(x) in F₁()

hence H₁(x) in F₁() by A9, FUNCOP_1:def 8; :: thesis: verum

end;

end;

end;

hence H₁(x) in F₁() ; :: thesis: verum

end;

consider F being Function of [:F₁(),NAT:],F₁() such that
A11: for x being object st x in [:F₁(),NAT:] holds
F . x = H₁(x) from FUNCT_2:sch 2(A7);
deffunc H₂( set ) -> Element of omega = 2;
consider D being DecoratedTree of F₁() such that
A12: D . {} = F₂() and
A13: for d being Element of dom D holds
( succ d = { (d ^ <*k*>) where k is Nat : k < H₂(D . d) } & ( for n being Nat st n < H₂(D . d) holds
D . (d ^ <*n*>) = F . ((D . d),n) ) ) from TREES_2:sch 9();

now :: thesis: for t being Element of dom D st not t in Leaves (dom D) holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of dom D; :: thesis: ( not t in Leaves (dom D) implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} )
assume not t in Leaves (dom D) ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
{ (t ^ <*k*>) where k is Nat : k < 2 } = {(t ^ <*0*>),(t ^ <*1*>)}

proof

thus { (t ^ <*k*>) where k is Nat : k < 2 } c= {(t ^ <*0*>),(t ^ <*1*>)} :: according to XBOOLE_0:def 10 :: thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*k*>) where k is Nat : k < 2 }

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { (t ^ <*k*>) where k is Nat : k < 2 } or v in {(t ^ <*0*>),(t ^ <*1*>)} )
assume v in { (t ^ <*k*>) where k is Nat : k < 2 } ; :: thesis: v in {(t ^ <*0*>),(t ^ <*1*>)}
then consider k being Nat such that
A14: v = t ^ <*k*> and
A15: k < 2 ;
( k = 0 or k = 1 ) by A15, NAT_1:23;
hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A14, TARSKI:def 2; :: thesis: verum

end;

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in {(t ^ <*0*>),(t ^ <*1*>)} or v in { (t ^ <*k*>) where k is Nat : k < 2 } )
assume v in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: v in { (t ^ <*k*>) where k is Nat : k < 2 }
then ( v = t ^ <*0*> or v = t ^ <*1*> ) by TARSKI:def 2;
hence v in { (t ^ <*k*>) where k is Nat : k < 2 } ; :: thesis: verum

end;

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A13; :: thesis: verum

end;

then dom D is binary by BINTREE1:def 2;
then reconsider D = D as binary DecoratedTree of F₁() by BINTREE1:def 3;
take D ; :: thesis: ( dom D = {0,1} * & D . {} = F₂() & ( for x being Node of D holds P₁[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )

now :: thesis: for t being Element of dom D holds succ t = {(t ^ <*0*>),(t ^ <*1*>)}

let t be Element of dom D; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
{ (t ^ <*k*>) where k is Nat : k < 2 } = {(t ^ <*0*>),(t ^ <*1*>)}

proof

thus { (t ^ <*k*>) where k is Nat : k < 2 } c= {(t ^ <*0*>),(t ^ <*1*>)} :: according to XBOOLE_0:def 10 :: thesis: {(t ^ <*0*>),(t ^ <*1*>)} c= { (t ^ <*k*>) where k is Nat : k < 2 }

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { (t ^ <*k*>) where k is Nat : k < 2 } or v in {(t ^ <*0*>),(t ^ <*1*>)} )
assume v in { (t ^ <*k*>) where k is Nat : k < 2 } ; :: thesis: v in {(t ^ <*0*>),(t ^ <*1*>)}
then consider k being Nat such that
A16: v = t ^ <*k*> and
A17: k < 2 ;
( k = 0 or k = 1 ) by A17, NAT_1:23;
hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A16, TARSKI:def 2; :: thesis: verum

end;

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in {(t ^ <*0*>),(t ^ <*1*>)} or v in { (t ^ <*k*>) where k is Nat : k < 2 } )
assume v in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: v in { (t ^ <*k*>) where k is Nat : k < 2 }
then ( v = t ^ <*0*> or v = t ^ <*1*> ) by TARSKI:def 2;
hence v in { (t ^ <*k*>) where k is Nat : k < 2 } ; :: thesis: verum

end;

hence succ t = {(t ^ <*0*>),(t ^ <*1*>)} by A13; :: thesis: verum

end;

hence dom D = {0,1} * by Th8; :: thesis: ( D . {} = F₂() & ( for x being Node of D holds P₁[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )
thus D . {} = F₂() by A12; :: thesis: for x being Node of D holds P₁[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)]
let x be Node of D; :: thesis: P₁[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)]
for e being set st e in F₁() holds
P₁[e,F . (e,0),F . (e,1)]

proof

let e be set ; :: thesis: ( e in F₁() implies P₁[e,F . (e,0),F . (e,1)] )
assume A18: e in F₁() ; :: thesis: P₁[e,F . (e,0),F . (e,1)]
then consider b, c being Element of F₁() such that
A19: P₁[e,b,c] and
A20: f . e = [b,c] by A6;
[e,1] in [:F₁(),NAT:] by A18, ZFMISC_1:87;
then A21: F . [e,1] = IFEQ (([e,1] `2),0,((f . ([e,1] `1)) `1),((f . ([e,1] `1)) `2)) by A11
.= (f . ([e,1] `1)) `2 by FUNCOP_1:def 8
.= (f . e) `2
.= c by A20 ;
[e,0] in [:F₁(),NAT:] by A18, ZFMISC_1:87;
then F . [e,0] = IFEQ (([e,0] `2),0,((f . ([e,0] `1)) `1),((f . ([e,0] `1)) `2)) by A11
.= (f . ([e,0] `1)) `1 by FUNCOP_1:def 8
.= (f . e) `1
.= b by A20 ;
hence P₁[e,F . (e,0),F . (e,1)] by A19, A21; :: thesis: verum

end;

then P₁[D . x,F . ((D . x),0),F . ((D . x),1)] ;
then P₁[D . x,D . (x ^ <*0*>),F . ((D . x),1)] by A13;
hence P₁[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] by A13; :: thesis: verum