let T0, T1 be Tree; :: thesis: for t being Element of tree (T0,T1) holds
( ( t = {} implies succ t = {(),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = ^ p holds
for sp being FinSequence holds
( sp in succ p iff ^ 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 ^ <*1*>)} ) & ( for p being Element of T0 st t = ^ p holds
for sp being FinSequence holds
( sp in succ p iff ^ 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 = ^ p holds
for sp being FinSequence holds
( sp in succ p iff ^ 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 ^ <*1*>)}
( {} in T1 & <*1*> = <*1*> ^ {} ) by ;
then <*1*> in tree (T0,T1) by TREES_3:68;
then A2: t ^ <*1*> in tree (T0,T1) by ;
A3: succ t = { (t ^ <*n*>) where n is Nat : t ^ <*n*> in tree (T0,T1) } by TREES_2:def 5;
( {} in T0 & = ^ {} ) by ;
then <*0*> in tree (T0,T1) by TREES_3:68;
then A4: t ^ in tree (T0,T1) by ;
now :: thesis: for x1 being object holds
( ( x1 in succ t implies x1 in {(),(t ^ <*1*>)} ) & ( x1 in {(),(t ^ <*1*>)} implies x1 in succ t ) )
let x1 be object ; :: thesis: ( ( x1 in succ t implies x1 in {(),(t ^ <*1*>)} ) & ( x1 in {(),(t ^ <*1*>)} implies x1 in succ t ) )
hereby :: thesis: ( x1 in {(),(t ^ <*1*>)} implies x1 in succ t )
assume x1 in succ t ; :: thesis: x1 in {(),(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 = ^ p ) or ( p in T1 & x = <*1*> ^ p ) ) by ;
then A7: ( x . 1 = 0 or x . 1 = 1 ) by FINSEQ_1:41;
x1 = <*n*> by ;
then ( x = or x = <*1*> ) by ;
then ( x = t ^ or x = t ^ <*1*> ) by ;
hence x1 in {(),(t ^ <*1*>)} by TARSKI:def 2; :: thesis: verum
end;
assume x1 in {(),(t ^ <*1*>)} ; :: thesis: x1 in succ t
then ( x1 = t ^ or x1 = t ^ <*1*> ) by TARSKI:def 2;
hence x1 in succ t by A3, A4, A2; :: thesis: verum
end;
hence succ t = {(),(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 = ^ p implies for sp being FinSequence holds
( ( sp in succ p implies ^ sp in succ t ) & ( ^ sp in succ t implies sp in succ p ) ) )

assume A8: t = ^ p ; :: thesis: for sp being FinSequence holds
( ( sp in succ p implies ^ sp in succ t ) & ( ^ sp in succ t implies sp in succ p ) )

let sp be FinSequence; :: thesis: ( ( sp in succ p implies ^ sp in succ t ) & ( ^ sp in succ t implies sp in succ p ) )
hereby :: thesis: ( ^ sp in succ t implies sp in succ p )
assume sp in succ p ; :: thesis: ^ 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 ;
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 ; :: thesis: verum
end;
set zsp = ^ 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 ;
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 = ^ (p ^ <*n*>) by ;
hence sp in succ p by ; :: 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 ;
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 ; :: 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 ;
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 ;
hence sp in succ p by ; :: thesis: verum