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