let p be FinSequence; :: thesis: ( p is Tree-yielding implies elementary_tree (len p) c= tree p )
assume A1: p is Tree-yielding ; :: thesis: elementary_tree (len p) c= tree p
then A2: rng p is constituted-Trees ;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in elementary_tree (len p) or q in tree p )
assume q in elementary_tree (len p) ; :: thesis: q in tree p
then ( q in { <*n*> where n is Nat : n < len p } or q in {{}} ) by XBOOLE_0:def 3;
then A3: ( ex n being Nat st
( q = <*n*> & n < len p ) or q = {} ) by TARSKI:def 1;
assume A4: not q in tree p ; :: thesis: contradiction
then consider n being Nat such that
A5: q = <*n*> and
A6: n < len p by A3, TREES_1:22;
p . (n + 1) in rng p by A6, Lm3;
then reconsider t = p . (n + 1) as Tree by A2;
A7: {} in t by TREES_1:22;
<*n*> ^ {} = q by A5, FINSEQ_1:34;
hence contradiction by A1, A4, A6, A7, Def15; :: thesis: verum