let n be Element of NAT ; :: thesis: for p, q being FinSequence st p is Tree-yielding holds
( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) )
let p, q be FinSequence; :: thesis: ( p is Tree-yielding implies ( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) ) )
assume A1: p is Tree-yielding ; :: thesis: ( <*n*> ^ q in tree p iff ( n < len p & q in p . (n + 1) ) )
thus ( <*n*> ^ q in tree p implies ( n < len p & q in p . (n + 1) ) ) :: thesis: ( n < len p & q in p . (n + 1) implies <*n*> ^ q in tree p )

proof

assume <*n*> ^ q in tree p ; :: thesis: ( n < len p & q in p . (n + 1) )
then consider k being Element of NAT , r being FinSequence such that
A2: k < len p and
A3: r in p . (k + 1) and
A4: <*n*> ^ q = <*k*> ^ r by A1, Def15;
A5: (<*n*> ^ q) . 1 = n by FINSEQ_1:41;
(<*k*> ^ r) . 1 = k by FINSEQ_1:41;
hence ( n < len p & q in p . (n + 1) ) by A2, A3, A4, A5, FINSEQ_1:33; :: thesis: verum

end;

thus ( n < len p & q in p . (n + 1) implies <*n*> ^ q in tree p ) by A1, Def15; :: thesis: verum