defpred S1[ object , object ] means ex b, c being Element of F1() st
( P1[$1,b,c] & $2 = [b,c] );
A2: for e being object st e in F1() holds
ex u being object st
( u in [:F1(),F1():] & S1[e,u] )
proof
let e be object ; :: thesis: ( e in F1() implies ex u being object st
( u in [:F1(),F1():] & S1[e,u] ) )
assume e in F1() ; :: thesis: ex u being object st
( u in [:F1(),F1():] & S1[e,u] )
then consider b, c being Element of F1() such that
A3: P1[e,b,c] by A1;
take u = [b,c]; :: thesis: ( u in [:F1(),F1():] & S1[e,u] )
thus u in [:F1(),F1():] ; :: thesis: S1[e,u]
thus S1[e,u] by A3; :: thesis: verum
end;
consider f being Function such that
A4: dom f = F1() and
A5: rng f c= [:F1(),F1():] and
A6: for e being object st e in F1() holds
S1[e,f . e] from FUNCT_1:sch 6(A2);
 deffunc H1( object ) -> object = IFEQ (($1 `2),0,((f . ($1 `1)) `1),((f . ($1 `1)) `2));
A7: for x being object st x in [:F1(),NAT:] holds
H1(x) in F1()
proof
let x be object ; :: thesis: ( x in [:F1(),NAT:] implies H1(x) in F1() )
assume x in [:F1(),NAT:] ; :: thesis: H1(x) in F1()
then x `1 in F1() 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 F1() by A5, MCART_1:10;
A10: (f . (x `1)) `1 in F1() by A5, A8, MCART_1:10;
now :: thesis: H1(x) in F1()
end;
hence H1(x) in F1() ; :: thesis: verum
end;
consider F being Function of [:F1(),NAT:],F1() such that
A11: for x being object st x in [:F1(),NAT:] holds
F . x = H1(x) from FUNCT_2:sch 2(A7);
 deffunc H2( set ) -> Element of omega = 2;
consider D being DecoratedTree of F1() such that
A12: D . {} = F2() and
A13: for d being Element of dom D holds
( succ d = { (d ^ <*k*>) where k is Nat : k < H2(D . d) } & ( for n being Nat st n < H2(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 F1() by BINTREE1:def 3;
take D ; :: thesis: ( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds P1[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 . {} = F2() & ( for x being Node of D holds P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )
thus D . {} = F2() by A12; :: thesis: for x being Node of D holds P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)]
let x be Node of D; :: thesis: P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)]
for e being set st e in F1() holds
P1[e,F . (e,0),F . (e,1)]
proof
let e be set ; :: thesis: ( e in F1() implies P1[e,F . (e,0),F . (e,1)] )
assume A18: e in F1() ; :: thesis: P1[e,F . (e,0),F . (e,1)]
then consider b, c being Element of F1() such that
A19: P1[e,b,c] and
A20: f . e = [b,c] by A6;
[e,1] in [:F1(),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 [:F1(),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 P1[e,F . (e,0),F . (e,1)] by A19, A21; :: thesis: verum
end;
then P1[D . x,F . ((D . x),0),F . ((D . x),1)] ;
then P1[D . x,D . (x ^ <*0*>),F . ((D . x),1)] by A13;
hence P1[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] by A13; :: thesis: verum