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

proof

let e be set ; :: thesis: ( e in F₁() implies ex u being set st
( u in [:F₁(),F₁():] & S₁[e,u] ) )
assume e in F₁() ; :: thesis: ex u being set 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 set st e in F₁() holds
S₁[e,f . e] from WELLORD2:sch 1(A2);
deffunc H₁( set ) -> set = IFEQ ($1 `2 ),0 ,((f . ($1 `1 )) `1 ),((f . ($1 `1 )) `2 );
A7: for x being set st x in [:F₁(),NAT :] holds
H₁(x) in F₁()

proof

let x be set ; :: 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 f . (x `1 ) in rng f by A4, FUNCT_1:def 5;
then A8: ( (f . (x `1 )) `1 in F₁() & (f . (x `1 )) `2 in F₁() ) by A5, MCART_1:10;

now

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

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

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

end;

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

hence H₁(x) in F₁() by A8, 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
A9: for x being set st x in [:F₁(),NAT :] holds
F . x = H₁(x) from FUNCT_2:sch 2(A7);
A10: 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 A11: e in F₁() ; :: thesis: P₁[e,F . e,0 ,F . e,1]
then consider b, c being Element of F₁() such that
A12: P₁[e,b,c] and
A13: f . e = [b,c] by A6;
A14: [e,0 ] `2 = 0 by MCART_1:7;
[e,0 ] in [:F<sub>1</sub>(),NAT :] by A11, ZFMISC_1:106;
then A15: F . [e,0 ] = IFEQ ([e,0 ] `2 ),0 ,((f . ([e,0 ] `1 )) `1 ),((f . ([e,0 ] `1 )) `2 ) by A9
.= (f . ([e,0 ] `1 )) `1 by A14, FUNCOP_1:def 8
.= (f . e) `1 by MCART_1:7
.= b by A13, MCART_1:7 ;
A16: ( [e,1] `2 = 1 & 1 <> 0 ) by MCART_1:7;
[e,1] in [:F₁(),NAT :] by A11, ZFMISC_1:106;
then F . [e,1] = IFEQ ([e,1] `2 ),0 ,((f . ([e,1] `1 )) `1 ),((f . ([e,1] `1 )) `2 ) by A9
.= (f . ([e,1] `1 )) `2 by A16, FUNCOP_1:def 8
.= (f . e) `2 by MCART_1:7
.= c by A13, MCART_1:7 ;
hence P₁[e,F . e,0 ,F . e,1] by A12, A15; :: thesis: verum

end;

deffunc H₂( set ) -> Element of NAT = 2;
consider D being DecoratedTree of such that
A17: D . {} = F₂() and
A18: for d being Element of dom D holds
( succ d = { (d ^ <*k*>) where k is Element of NAT : k < H₂(D . d) } & ( for n being Element of NAT st n < H₂(D . d) holds
D . (d ^ <*n*>) = F . (D . d),n ) ) from TREES_2:sch 9();

now

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 Element of NAT : k < 2 } = {(t ^ <*0 *>),(t ^ <*1*>)}

proof

thus { (t ^ <*k*>) where k is Element of 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 Element of NAT : k < 2 }

proof

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

end;

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

end;

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

end;

then dom D is binary by BINTREE1:def 2;
then reconsider D = D as binary DecoratedTree of 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

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

proof

thus { (t ^ <*k*>) where k is Element of 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 Element of NAT : k < 2 }

proof

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

end;

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

end;

hence succ t = {(t ^ <*0 *>),(t ^ <*1*>)} by A18; :: 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 A17; :: 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*>)]
P₁[D . x,F . (D . x),0 ,F . (D . x),1] by A10;
then P₁[D . x,D . (x ^ <*0 *>),F . (D . x),1] by A18;
hence P₁[D . x,D . (x ^ <*0 *>),D . (x ^ <*1*>)] by A18; :: thesis: verum