set e = elementary_tree 2;
let Z be Tree; :: thesis:
let x1, x2 be Element of Z; :: thesis:
assume that
A1: x1 = <*0*> and
A2: x2 = <*1*> and
A3: succ (Root Z) = {x1,x2} ; :: thesis:
set T1 = (elementary_tree 2) with-replacement (<*0*>,(Z | x1));
A4: <*0*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:53;

A5: now :: thesis:

let s be FinSequence of NAT ; :: thesis:
thus ( not s in Z or ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) :: thesis:

proof

assume A6: s in Z ; :: thesis:

per cases ;

suppose s = {} ; :: thesis:

hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by TREES_1:22; :: thesis:

end;

suppose s <> {} ; :: thesis:

then consider w being FinSequence of NAT , n being Element of NAT such that
A7: s = <*n*> ^ w by FINSEQ_2:130;
<*n*> is_a_prefix_of s by A7, TREES_1:1;
then A8: <*n*> in Z by A6, TREES_1:20;
<*n*> = (Root Z) ^ <*n*> by FINSEQ_1:34;
then A9: <*n*> in succ (Root Z) by A8, TREES_2:12;

now :: thesis:

per cases = <*0*> or <*n*> = <*1*> ) by A1, A2, A3, A9, TARSKI:def 2;

suppose A10: <*n*> = <*0*> ; :: thesis:

then w in Z | x1 by A1, A6, A7, TREES_1:def 6;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A4, A7, A10, Th2, TREES_1:def 9; :: thesis:

end;

suppose A11: <*n*> = <*1*> ; :: thesis:

then w in Z | x2 by A2, A6, A7, TREES_1:def 6;
hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) by A7, A11; :: thesis:

end;

end;

end;

hence ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; :: thesis:

end;

end;

end;

assume A12: ( ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) or ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ) ; :: thesis:

now :: thesis:

per cases by A12;

suppose A13: ( s in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) & not <*1*> is_a_proper_prefix_of s ) ; :: thesis:

now :: thesis:

per cases by A4, A13, TREES_1:def 9;

suppose ( s in elementary_tree 2 & not <*0*> is_a_proper_prefix_of s ) ; :: thesis:

then ( s = {} or s = <*0*> or s = <*1*> ) by ENUMSET1:def 1, TREES_1:53;
hence s in Z by A1, A2, A3; :: thesis:

end;

suppose ex w being FinSequence of NAT st
( w in Z | x1 & s = <*0*> ^ w ) ; :: thesis:

hence s in Z by A1, TREES_1:def 6; :: thesis:

end;

end;

end;

hence s in Z ; :: thesis:

end;

suppose ex w being FinSequence of NAT st
( w in Z | x2 & s = <*1*> ^ w ) ; :: thesis:

hence s in Z by A2, TREES_1:def 6; :: thesis:

end;

end;

end;

hence s in Z ; :: thesis:

end;

A14: not <*0*> is_a_proper_prefix_of <*1*> by TREES_1:3;
<*1*> in elementary_tree 2 by ENUMSET1:def 1, TREES_1:53;
then <*1*> in (elementary_tree 2) with-replacement (<*0*>,(Z | x1)) by A4, A14, TREES_1:def 9;
hence Z = ((elementary_tree 2) with-replacement (<*0*>,(Z | x1))) with-replacement (<*1*>,(Z | x2)) by A5, TREES_1:def 9; :: thesis: