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

defpred S_{1}[ object , object ] means ( ( $1 `2 = 0 implies P_{1}[$1 `1 ,$2] ) & ( $1 `2 = 1 implies P_{2}[$1 `1 ,$2] ) );

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

ex u being object st

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

A6: ( dom F = [:F_{1}(),NAT:] & rng F c= F_{1}() )
and

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

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

reconsider F = F as Function of [:F_{1}(),NAT:],F_{1}() by A6, FUNCT_2:2;

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

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

A9: for d being Element of dom D holds

( succ d = { (d ^ <*k*>) where k is Nat : k < H_{1}(D . d) } & ( for n being Nat st n < H_{1}(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*>)] & P_{2}[D . x,D . (x ^ <*1*>)] ) ) )

_{2}() & ( for x being Node of D holds

( P_{1}[D . x,D . (x ^ <*0*>)] & P_{2}[D . x,D . (x ^ <*1*>)] ) ) )

thus D . {} = F_{2}()
by A8; :: thesis: for x being Node of D holds

( P_{1}[D . x,D . (x ^ <*0*>)] & P_{2}[D . x,D . (x ^ <*1*>)] )

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

[(D . x),0] `2 = 0 ;

then P_{1}[[(D . x),0] `1 ,F . [(D . x),0]]
by A7;

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

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

[(D . x),1] `2 = 1 ;

then P_{2}[[(D . x),1] `1 ,F . [(D . x),1]]
by A7;

then P_{2}[D . x,F . ((D . x),1)]
;

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

defpred S

A3: 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}(),NAT:] implies ex u being object st

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

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

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

then reconsider e1 = e `1 as Element of F_{1}() by MCART_1:10;

consider u1 being Element of F_{1}() such that

A4: P_{1}[e1,u1]
by A1;

consider u2 being Element of F_{1}() such that

A5: P_{2}[e1,u2]
by A2;

take u = IFEQ ((e `2),0,u1,u2); :: thesis: ( u in F_{1}() & S_{1}[e,u] )

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

thus ( e `2 = 0 implies P_{1}[e `1 ,u] )
by A4, FUNCOP_1:def 8; :: thesis: ( e `2 = 1 implies P_{2}[e `1 ,u] )

thus ( e `2 = 1 implies P_{2}[e `1 ,u] )
by A5, FUNCOP_1:def 8; :: thesis: verum

end;( u in F

assume e in [:F

( u in F

then reconsider e1 = e `1 as Element of F

consider u1 being Element of F

A4: P

consider u2 being Element of F

A5: P

take u = IFEQ ((e `2),0,u1,u2); :: thesis: ( u in F

thus u in F

thus ( e `2 = 0 implies P

thus ( e `2 = 1 implies P

A6: ( dom F = [:F

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

S

reconsider F = F as Function of [:F

consider D being DecoratedTree of F

A8: D . {} = F

A9: 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 A9; :: 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

A10: v = t ^ <*k*> and

A11: k < 2 ;

( k = 0 or k = 1 ) by A11, NAT_1:23;

hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A10, 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

A10: v = t ^ <*k*> and

A11: k < 2 ;

( k = 0 or k = 1 ) by A11, NAT_1:23;

hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A10, 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

( P

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 A9; :: 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

A12: v = t ^ <*k*> and

A13: k < 2 ;

( k = 0 or k = 1 ) by A13, NAT_1:23;

hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A12, 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

A12: v = t ^ <*k*> and

A13: k < 2 ;

( k = 0 or k = 1 ) by A13, NAT_1:23;

hence v in {(t ^ <*0*>),(t ^ <*1*>)} by A12, 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

( P

thus D . {} = F

( P

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

[(D . x),0] `2 = 0 ;

then P

then P

hence P

[(D . x),1] `2 = 1 ;

then P

then P

hence P