defpred S_{1}[ object , object ] means ex b, c being Element of F_{1}() st

( P_{1}[$1,b,c] & $2 = [b,c] );

A2: for e being object st e in F_{1}() holds

ex u being object st

( u in [:F_{1}(),F_{1}():] & S_{1}[e,u] )

A4: dom f = F_{1}()
and

A5: rng f c= [:F_{1}(),F_{1}():]
and

A6: for e being object st e in F_{1}() holds

S_{1}[e,f . e]
from FUNCT_1:sch 6(A2);

deffunc H_{1}( object ) -> object = IFEQ (($1 `2),0,((f . ($1 `1)) `1),((f . ($1 `1)) `2));

A7: for x being object st x in [:F_{1}(),NAT:] holds

H_{1}(x) in F_{1}()
_{1}(),NAT:],F_{1}() such that

A11: for x being object st x in [:F_{1}(),NAT:] holds

F . x = H_{1}(x)
from FUNCT_2:sch 2(A7);

deffunc H_{2}( set ) -> Element of omega = 2;

consider D being DecoratedTree of F_{1}() such that

A12: D . {} = F_{2}()
and

A13: for d being Element of dom D holds

( succ d = { (d ^ <*k*>) where k is Nat : k < H_{2}(D . d) } & ( for n being Nat st n < H_{2}(D . d) holds

D . (d ^ <*n*>) = F . ((D . d),n) ) ) from TREES_2:sch 9();

then reconsider D = D as binary DecoratedTree of F_{1}() by BINTREE1:def 3;

take D ; :: thesis: ( dom D = {0,1} * & D . {} = F_{2}() & ( for x being Node of D holds P_{1}[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )

_{2}() & ( for x being Node of D holds P_{1}[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)] ) )

thus D . {} = F_{2}()
by A12; :: thesis: for x being Node of D holds P_{1}[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)]

let x be Node of D; :: thesis: P_{1}[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)]

for e being set st e in F_{1}() holds

P_{1}[e,F . (e,0),F . (e,1)]
_{1}[D . x,F . ((D . x),0),F . ((D . x),1)]
;

then P_{1}[D . x,D . (x ^ <*0*>),F . ((D . x),1)]
by A13;

hence P_{1}[D . x,D . (x ^ <*0*>),D . (x ^ <*1*>)]
by A13; :: thesis: verum

( P

A2: for e being object st e in F

ex u being object st

( u in [:F

proof

consider f being Function such that
let e be object ; :: thesis: ( e in F_{1}() implies ex u being object st

( u in [:F_{1}(),F_{1}():] & S_{1}[e,u] ) )

assume e in F_{1}()
; :: thesis: ex u being object st

( u in [:F_{1}(),F_{1}():] & S_{1}[e,u] )

then consider b, c being Element of F_{1}() such that

A3: P_{1}[e,b,c]
by A1;

take u = [b,c]; :: thesis: ( u in [:F_{1}(),F_{1}():] & S_{1}[e,u] )

thus u in [:F_{1}(),F_{1}():]
; :: thesis: S_{1}[e,u]

thus S_{1}[e,u]
by A3; :: thesis: verum

end;( u in [:F

assume e in F

( u in [:F

then consider b, c being Element of F

A3: P

take u = [b,c]; :: thesis: ( u in [:F

thus u in [:F

thus S

A4: dom f = F

A5: rng f c= [:F

A6: for e being object st e in F

S

deffunc H

A7: for x being object st x in [:F

H

proof

consider F being Function of [:F
let x be object ; :: thesis: ( x in [:F_{1}(),NAT:] implies H_{1}(x) in F_{1}() )

assume x in [:F_{1}(),NAT:]
; :: thesis: H_{1}(x) in F_{1}()

then x `1 in F_{1}()
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_{1}()
by A5, MCART_1:10;

A10: (f . (x `1)) `1 in F_{1}()
by A5, A8, MCART_1:10;

hence H_{1}(x) in F_{1}()
; :: thesis: verum

end;assume x in [:F

then x `1 in F

then A8: f . (x `1) in rng f by A4, FUNCT_1:def 3;

then A9: (f . (x `1)) `2 in F

A10: (f . (x `1)) `1 in F

hence H

A11: for x being object st x in [:F

F . x = H

deffunc H

consider D being DecoratedTree of F

A12: D . {} = F

A13: for d being Element of dom D holds

( succ d = { (d ^ <*k*>) where k is Nat : k < H

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*>)}

then
dom D is binary
by BINTREE1:def 2;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*>)}

end;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

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by A13; :: thesis: verum
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 }

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;proof

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 } )
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;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

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

then reconsider D = D as binary DecoratedTree of F

take D ; :: thesis: ( dom D = {0,1} * & D . {} = F

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

hence
dom D = {0,1} *
by Th8; :: thesis: ( D . {} = Flet 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*>)}

end;{ (t ^ <*k*>) where k is Nat : k < 2 } = {(t ^ <*0*>),(t ^ <*1*>)}

proof

hence
succ t = {(t ^ <*0*>),(t ^ <*1*>)}
by A13; :: thesis: verum
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 }

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;proof

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 } )
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;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

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

thus D . {} = F

let x be Node of D; :: thesis: P

for e being set st e in F

P

proof

then
P
let e be set ; :: thesis: ( e in F_{1}() implies P_{1}[e,F . (e,0),F . (e,1)] )

assume A18: e in F_{1}()
; :: thesis: P_{1}[e,F . (e,0),F . (e,1)]

then consider b, c being Element of F_{1}() such that

A19: P_{1}[e,b,c]
and

A20: f . e = [b,c] by A6;

[e,1] in [:F_{1}(),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_{1}(),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_{1}[e,F . (e,0),F . (e,1)]
by A19, A21; :: thesis: verum

end;assume A18: e in F

then consider b, c being Element of F

A19: P

A20: f . e = [b,c] by A6;

[e,1] in [:F

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

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

then P

hence P