let T0, T1 be Tree; :: thesis: for t being Element of tree (T0,T1) holds
( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t ) ) )
let t be Element of tree (T0,T1); :: thesis: ( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t ) ) )
set RT = tree (T0,T1);

hereby :: thesis: ( ( for p being Element of T0 st t = <*0*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t ) ) )

assume A1: t = {} ; :: thesis: succ t = {(t ^ <*0*>),(t ^ <*1*>)}
( {} in T1 & <*1*> = <*1*> ^ {} ) by FINSEQ_1:34, TREES_1:22;
then <*1*> in tree (T0,T1) by TREES_3:68;
then A2: t ^ <*1*> in tree (T0,T1) by A1, FINSEQ_1:34;
A3: succ t = { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;
( {} in T0 & <*0*> = <*0*> ^ {} ) by FINSEQ_1:34, TREES_1:22;
then <*0*> in tree (T0,T1) by TREES_3:68;
then A4: t ^ <*0*> in tree (T0,T1) by A1, FINSEQ_1:34;

now :: thesis: for x1 being object holds
( ( x1 in succ t implies x1 in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x1 in {(t ^ <*0*>),(t ^ <*1*>)} implies x1 in succ t ) )

let x1 be object ; :: thesis: ( ( x1 in succ t implies x1 in {(t ^ <*0*>),(t ^ <*1*>)} ) & ( x1 in {(t ^ <*0*>),(t ^ <*1*>)} implies x1 in succ t ) )

hereby :: thesis: ( x1 in {(t ^ <*0*>),(t ^ <*1*>)} implies x1 in succ t )

assume x1 in succ t ; :: thesis: x1 in {(t ^ <*0*>),(t ^ <*1*>)}
then consider n being Nat such that
A5: x1 = t ^ <*n*> and
A6: t ^ <*n*> in tree (T0,T1) by A3;
reconsider x = x1 as FinSequence by A5;
ex p being FinSequence st
( ( p in T0 & x = <*0*> ^ p ) or ( p in T1 & x = <*1*> ^ p ) ) by A5, A6, TREES_3:68;
then A7: ( x . 1 = 0 or x . 1 = 1 ) by FINSEQ_1:41;
x1 = <*n*> by A1, A5, FINSEQ_1:34;
then ( x = <*0*> or x = <*1*> ) by A7;
then ( x = t ^ <*0*> or x = t ^ <*1*> ) by A1, FINSEQ_1:34;
hence x1 in {(t ^ <*0*>),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum

end;

assume x1 in {(t ^ <*0*>),(t ^ <*1*>)} ; :: thesis: x1 in succ t
then ( x1 = t ^ <*0*> or x1 = t ^ <*1*> ) by TARSKI:def 2;
hence x1 in succ t by A3, A4, A2; :: thesis: verum

end;

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

end;

hereby :: thesis: for p being Element of T1 st t = <*1*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t )

let p be Element of T0; :: thesis: ( t = <*0*> ^ p implies for sp being FinSequence holds
( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) ) )
assume A8: t = <*0*> ^ p ; :: thesis: for sp being FinSequence holds
( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) )
let sp be FinSequence; :: thesis: ( ( sp in succ p implies <*0*> ^ sp in succ t ) & ( <*0*> ^ sp in succ t implies sp in succ p ) )

hereby :: thesis: ( <*0*> ^ sp in succ t implies sp in succ p )

assume sp in succ p ; :: thesis: <*0*> ^ sp in succ t
then sp in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T0 } by TREES_2:def 5;
then consider n being Nat such that
A9: sp = p ^ <*n*> and
A10: p ^ <*n*> in T0 ;
<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A10, TREES_3:69;
then (<*0*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;
then t ^ <*n*> in { (t ^ <*k*>) where k is Nat : t ^ <*k*> in tree (T0,T1) } by A8;
then t ^ <*n*> in succ t by TREES_2:def 5;
hence <*0*> ^ sp in succ t by A8, A9, FINSEQ_1:32; :: thesis: verum

end;

set zsp = <*0*> ^ sp;
assume <*0*> ^ sp in succ t ; :: thesis: sp in succ p
then <*0*> ^ sp in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;
then consider n being Nat such that
A11: <*0*> ^ sp = t ^ <*n*> and
A12: t ^ <*n*> in tree (T0,T1) ;
<*0*> ^ (p ^ <*n*>) in tree (T0,T1) by A8, A12, FINSEQ_1:32;
then p ^ <*n*> in T0 by TREES_3:69;
then p ^ <*n*> in { (p ^ <*k*>) where k is Nat : p ^ <*k*> in T0 } ;
then A13: p ^ <*n*> in succ p by TREES_2:def 5;
<*0*> ^ sp = <*0*> ^ (p ^ <*n*>) by A8, A11, FINSEQ_1:32;
hence sp in succ p by A13, FINSEQ_1:33; :: thesis: verum

end;

let p be Element of T1; :: thesis: ( t = <*1*> ^ p implies for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t ) )
assume A14: t = <*1*> ^ p ; :: thesis: for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t )
let sp be FinSequence; :: thesis: ( sp in succ p iff <*1*> ^ sp in succ t )

hereby :: thesis: ( <*1*> ^ sp in succ t implies sp in succ p )

assume sp in succ p ; :: thesis: <*1*> ^ sp in succ t
then sp in { (p ^ <*n*>) where n is Nat : p ^ <*n*> in T1 } by TREES_2:def 5;
then consider n being Nat such that
A15: sp = p ^ <*n*> and
A16: p ^ <*n*> in T1 ;
<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A16, TREES_3:70;
then (<*1*> ^ p) ^ <*n*> in tree (T0,T1) by FINSEQ_1:32;
then t ^ <*n*> in { (t ^ <*k*>) where k is Nat : t ^ <*k*> in tree (T0,T1) } by A14;
then t ^ <*n*> in succ t by TREES_2:def 5;
hence <*1*> ^ sp in succ t by A14, A15, FINSEQ_1:32; :: thesis: verum

end;

set zsp = <*1*> ^ sp;
assume <*1*> ^ sp in succ t ; :: thesis: sp in succ p
then <*1*> ^ sp in { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;
then consider n being Nat such that
A17: <*1*> ^ sp = t ^ <*n*> and
A18: t ^ <*n*> in tree (T0,T1) ;
<*1*> ^ (p ^ <*n*>) in tree (T0,T1) by A14, A18, FINSEQ_1:32;
then p ^ <*n*> in T1 by TREES_3:70;
then p ^ <*n*> in { (p ^ <*k*>) where k is Nat : p ^ <*k*> in T1 } ;
then A19: p ^ <*n*> in succ p by TREES_2:def 5;
<*1*> ^ sp = <*1*> ^ (p ^ <*n*>) by A14, A17, FINSEQ_1:32;
hence sp in succ p by A19, FINSEQ_1:33; :: thesis: verum