let p be Tree-yielding FinSequence; :: thesis: tree (p ^ <*(elementary_tree 0 )*>) = (tree p) \/ (elementary_tree ((len p) + 1))
len p < (len p) + 1 by NAT_1:13;
then A1: <*(len p)*> in elementary_tree ((len p) + 1) by TREES_1:55;
then A2: <*(len p)*> in (tree p) \/ (elementary_tree ((len p) + 1)) by XBOOLE_0:def 3;
{} in (elementary_tree ((len p) + 1)) | <*(len p)*> by TREES_1:47;
then A3: elementary_tree 0 c= (elementary_tree ((len p) + 1)) | <*(len p)*> by TREES_1:56, ZFMISC_1:37;
A4: (elementary_tree ((len p) + 1)) | <*(len p)*> c= elementary_tree 0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (elementary_tree ((len p) + 1)) | <*(len p)*> or x in elementary_tree 0 )
assume x in (elementary_tree ((len p) + 1)) | <*(len p)*> ; :: thesis: x in elementary_tree 0
then reconsider q = x as Element of (elementary_tree ((len p) + 1)) | <*(len p)*> ;
( <*(len p)*> ^ q <> {} & <*(len p)*> ^ q in elementary_tree ((len p) + 1) ) by A1, TREES_1:def 9;
then consider n being Element of NAT such that
A5: ( n < (len p) + 1 & <*(len p)*> ^ q = <*n*> ) by TREES_1:57;
( len <*n*> = 1 & len <*(len p)*> = 1 ) by FINSEQ_1:57;
then 1 + (len q) = 1 + 0 by A5, FINSEQ_1:35;
then x = {} ;
hence x in elementary_tree 0 by TREES_1:47; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: for r being FinSequence st <*(len p)*> = <*n*> ^ r holds
not n < len p
let r be FinSequence; :: thesis: ( <*(len p)*> = <*n*> ^ r implies not n < len p )
assume <*(len p)*> = <*n*> ^ r ; :: thesis: not n < len p
then n = <*(len p)*> . 1 by FINSEQ_1:58
.= len p by FINSEQ_1:57 ;
hence not n < len p ; :: thesis: verum

end;

then for n being Element of NAT
for q being FinSequence holds
( not n < len p or not q in p . (n + 1) or not <*(len p)*> = <*n*> ^ q ) ;
then not <*(len p)*> in tree p by Def15;
then A6: ((tree p) \/ (elementary_tree ((len p) + 1))) | <*(len p)*> = (elementary_tree ((len p) + 1)) | <*(len p)*> by A2, Th50
.= elementary_tree 0 by A3, A4, XBOOLE_0:def 10 ;
thus tree (p ^ <*(elementary_tree 0 )*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement <*(len p)*>,(elementary_tree 0 ) by Th58
.= (tree p) \/ (elementary_tree ((len p) + 1)) by A2, A6, TREES_2:8 ; :: thesis: verum