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:28;
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:22;
then A3: elementary_tree 0 c= (elementary_tree ((len p) + 1)) | <*(len p)*> by TREES_1:29, ZFMISC_1:31;
A4: (elementary_tree ((len p) + 1)) | <*(len p)*> c= elementary_tree 0

proof

let x be object ; :: 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 in elementary_tree ((len p) + 1) by A1, TREES_1:def 6;
then consider n being Nat such that
n < (len p) + 1 and
A5: <*(len p)*> ^ q = <*n*> by TREES_1:30;
A6: len <*n*> = 1 by FINSEQ_1:40;
len <*(len p)*> = 1 by FINSEQ_1:40;
then 1 + (len q) = 1 + 0 by A5, A6, FINSEQ_1:22;
then x = {} ;
hence x in elementary_tree 0 by TREES_1:22; :: thesis: verum

end;

now :: thesis: for n being Nat
for r being FinSequence st <*(len p)*> = <*n*> ^ r holds
not n < len p

let n be 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:41
.= len p ;
hence not n < len p ; :: thesis: verum

end;

then for n being 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 A7: ((tree p) \/ (elementary_tree ((len p) + 1))) | <*(len p)*> = (elementary_tree ((len p) + 1)) | <*(len p)*> by A2, Th47
.= elementary_tree 0 by A3, A4 ;
thus tree (p ^ <*(elementary_tree 0)*>) = ((tree p) \/ (elementary_tree ((len p) + 1))) with-replacement (<*(len p)*>,(elementary_tree 0)) by Th55
.= (tree p) \/ (elementary_tree ((len p) + 1)) by A2, A7, TREES_2:6 ; :: thesis: verum